lemma le_rewl: ∀E:ordered_set.∀z,y,x:E. x ≈ y → x ≤ z → y ≤ z.
intros (E z y x Exy Lxz); apply (le_transitive ???? ? Lxz);
lemma le_rewl: ∀E:ordered_set.∀z,y,x:E. x ≈ y → x ≤ z → y ≤ z.
intros (E z y x Exy Lxz); apply (le_transitive ???? ? Lxz);
lemma ap_rewl: ∀A:bishop_set.∀x,z,y:A. x ≈ y → y # z → x # z.
intros (A x z y Exy Ayz); cases (bs_cotransitive ???x Ayz); [2:assumption]
lemma ap_rewl: ∀A:bishop_set.∀x,z,y:A. x ≈ y → y # z → x # z.
intros (A x z y Exy Ayz); cases (bs_cotransitive ???x Ayz); [2:assumption]
cases Exy; right; assumption;
qed.
lemma exc_rewr: ∀A:ordered_set.∀x,z,y:A. x ≈ y → z ≰ y → z ≰ x.
cases Exy; right; assumption;
qed.
lemma exc_rewr: ∀A:ordered_set.∀x,z,y:A. x ≈ y → z ≰ y → z ≰ x.
cases (Exy); left; assumption;
qed.
notation > "'Ex'≪" non associative with precedence 50 for @{'ordered_setrewritel}.
cases (Exy); left; assumption;
qed.
notation > "'Ex'≪" non associative with precedence 50 for @{'ordered_setrewritel}.