From 93822eb2767be2cfb2f15d88d4d8c9e7595af1ca Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 15 Nov 2007 17:13:51 +0000 Subject: [PATCH] declared eq_sym as a coercion and added 2 lemmas for rewriting # --- helm/software/matita/dama/excedence.ma | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/helm/software/matita/dama/excedence.ma b/helm/software/matita/dama/excedence.ma index 4931e70d2..84a033c3a 100644 --- a/helm/software/matita/dama/excedence.ma +++ b/helm/software/matita/dama/excedence.ma @@ -84,11 +84,16 @@ intros (E); unfold; intros (x y Exy); unfold; unfold; intros (Ayx); apply Exy; apply ap_symmetric; assumption; qed. +lemma eq_symmetric_:∀E:apartness.∀x,y:E.x ≈ y → y ≈ x := eq_symmetric. + +coercion cic:/matita/excedence/eq_symmetric_.con. + lemma eq_transitive: ∀E.transitive ? (eq E). (* bug. intros k deve fare whd quanto basta *) intros 6 (E x y z Exy Eyz); intro Axy; cases (ap_cotransitive ???y Axy); [apply Exy|apply Eyz] assumption. qed. + (* BUG: vedere se ricapita *) lemma le_antisymmetric: ∀E.antisymmetric ? (le E) (eq ?). intros 5 (E x y Lxy Lyx); intro H; @@ -137,3 +142,13 @@ lemma le_rewr: ∀E:excedence.∀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. + +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] +cases (Exy (ap_symmetric ??? a)); +qed. + +lemma ap_rewr: ∀A:apartness.∀x,z,y:A. x ≈ y → z # y → z # x. +intros (A x z y Exy Azy); apply ap_symmetric; apply (ap_rewl ???? Exy); +apply ap_symmetric; assumption; +qed. -- 2.39.2