+coercion hint2 nocomposites.
+*)
+
+
+notation "r \sup *" non associative with precedence 90 for @{'OR_f_star $r}.
+notation > "r *" non associative with precedence 90 for @{'OR_f_star $r}.
+
+notation "r \sup (⎻* )" non associative with precedence 90 for @{'OR_f_minus_star $r}.
+notation > "r⎻*" non associative with precedence 90 for @{'OR_f_minus_star $r}.
+
+notation "r \sup ⎻" non associative with precedence 90 for @{'OR_f_minus $r}.
+notation > "r⎻" non associative with precedence 90 for @{'OR_f_minus $r}.
+
+interpretation "o-relation f⎻*" 'OR_f_minus_star r = (fun_1 __ (or_f_minus_star _ _) r).
+interpretation "o-relation f⎻" 'OR_f_minus r = (fun_1 __ (or_f_minus _ _) r).
+interpretation "o-relation f*" 'OR_f_star r = (fun_1 __ (or_f_star _ _) r).
+
+definition or_prop1 : ∀P,Q:OAlgebra.∀F:ORelation_setoid P Q.∀p,q.
+ (F p ≤ q) = (p ≤ F* q).
+intros; apply (or_prop1_ ?? F p q);
+qed.
+
+definition or_prop2 : ∀P,Q:OAlgebra.∀F:ORelation_setoid P Q.∀p,q.
+ (F⎻ p ≤ q) = (p ≤ F⎻* q).
+intros; apply (or_prop2_ ?? F p q);
+qed.
+
+definition or_prop3 : ∀P,Q:OAlgebra.∀F:ORelation_setoid P Q.∀p,q.
+ (F p >< q) = (p >< F⎻ q).
+intros; apply (or_prop3_ ?? F p q);
+qed.