intro Xyz; apply Exy; apply unfold_apart; right; assumption;
qed.
-notation > "'Ex'≪" non associative with precedence 50 for
- @{'excessrewritel}.
-
-interpretation "exc_rewl" 'excessrewritel =
- (cic:/matita/excess/exc_rewl.con _ _ _).
-
lemma le_rewr: ∀E:excess.∀z,y,x:E. x ≈ y → z ≤ x → z ≤ y.
intros (E z y x Exy Lxz); apply (le_transitive ???? Lxz);
intro Xyz; apply Exy; apply unfold_apart; left; assumption;
qed.
-notation > "'Ex'≫" non associative with precedence 50 for
- @{'excessrewriter}.
+notation > "'Le'≪" non associative with precedence 50 for
+ @{'lerewritel}.
-interpretation "exc_rewr" 'excessrewriter =
- (cic:/matita/excess/exc_rewr.con _ _ _).
+interpretation "le_rewl" 'lerewritel =
+ (cic:/matita/excess/le_rewl.con _ _ _).
+
+notation > "'Le'≫" non associative with precedence 50 for
+ @{'lerewriter}.
+
+interpretation "le_rewr" 'lerewriter =
+ (cic:/matita/excess/le_rewr.con _ _ _).
lemma ap_rewl: ∀A:apartness.∀x,z,y:A. x ≈ y → y # z → x # z.
intros (A x z y Exy Ayz); cases (ap_cotransitive ???x Ayz); [2:assumption]
elim (Exy); left; assumption;
qed.
+notation > "'Ex'≪" non associative with precedence 50 for
+ @{'excessrewritel}.
+
+interpretation "exc_rewl" 'excessrewritel =
+ (cic:/matita/excess/exc_rewl.con _ _ _).
+
+notation > "'Ex'≫" non associative with precedence 50 for
+ @{'excessrewriter}.
+
+interpretation "exc_rewr" 'excessrewriter =
+ (cic:/matita/excess/exc_rewr.con _ _ _).
+
lemma lt_rewr: ∀A:excess.∀x,z,y:A. x ≈ y → z < y → z < x.
intros (A x y z E H); split; elim H;
[apply (le_rewr ???? (eq_sym ??? E));|apply (ap_rewr ???? E)] assumption;
[apply (le_rewl ???? (eq_sym ??? E));| apply (ap_rewl ???? E);] assumption;
qed.
+notation > "'Lt'≪" non associative with precedence 50 for
+ @{'ltrewritel}.
+
+interpretation "lt_rewl" 'ltrewritel =
+ (cic:/matita/excess/lt_rewl.con _ _ _).
+
+notation > "'Lt'≫" non associative with precedence 50 for
+ @{'ltrewriter}.
+
+interpretation "lt_rewr" 'ltrewriter =
+ (cic:/matita/excess/lt_rewr.con _ _ _).
+
lemma lt_le_transitive: ∀A:excess.∀x,y,z:A.x < y → y ≤ z → x < z.
intros (A x y z LT LE); cases LT (LEx APx); split; [apply (le_transitive ???? LEx LE)]
whd in LE LEx APx; cases APx (EXx EXx); [cases (LEx EXx)]