exhaustivity defined

[helm.git] / helm / software / matita / contribs / dama / dama / bishop_set_rewrite.ma

diff --git a/helm/software/matita/contribs/dama/dama/bishop_set_rewrite.ma b/helm/software/matita/contribs/dama/dama/bishop_set_rewrite.ma
index bd5a83a8843cc4f7d27308be89f94b17f1e88d20..19518a67b6f29eb593a177f8d7817aba5863ea6e 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/bishop_set_rewrite.ma
+++ b/helm/software/matita/contribs/dama/dama/bishop_set_rewrite.ma
@@ -70,3 +70,19 @@ interpretation "exc_rewl" 'ordered_setrewritel = (cic:/matita/dama/bishop_set_re
 notation > "'Ex'≫" non associative with precedence 50 for @{'ordered_setrewriter}.
 interpretation "exc_rewr" 'ordered_setrewriter = (cic:/matita/dama/bishop_set_rewrite/exc_rewr.con _ _ _).
 
+
+lemma lt_rewr: ∀A:ordered_set.∀x,z,y:A. x ≈ y → z < y → z < x.
+intros (A x y z E H); split; cases H;
+[apply (Le≫ ? (eq_sym ??? E));|apply (Ap≫ ? E)] assumption;
+qed.
+
+lemma lt_rewl: ∀A:ordered_set.∀x,z,y:A. x ≈ y → y < z → x < z.
+intros (A x y z E H); split; cases H;
+[apply (Le≪ ? (eq_sym ??? E));| apply (Ap≪ ? E);] assumption;
+qed.
+
+notation > "'Lt'≪" non associative with precedence 50 for @{'ltrewritel}.
+interpretation "lt_rewl" 'ltrewritel = (cic:/matita/dama/bishop_set_rewrite/lt_rewl.con _ _ _).
+notation > "'Lt'≫" non associative with precedence 50 for @{'ltrewriter}.
+interpretation "lt_rewr" 'ltrewriter = (cic:/matita/dama/bishop_set_rewrite/lt_rewr.con _ _ _).
+