snopshot before isabellization

[helm.git] / helm / software / matita / dama / excess.ma

diff --git a/helm/software/matita/dama/excess.ma b/helm/software/matita/dama/excess.ma
index 55f531a9b53f7ff5016d16b42323cfa914555bb8..0f236dd06a3ea4b3463740b52be6f23d9620086d 100644 (file)
--- a/helm/software/matita/dama/excess.ma
+++ b/helm/software/matita/dama/excess.ma
@@ -258,3 +258,10 @@ qed.
 
 definition total_order_property : ∀E:excess. Type ≝
   λE:excess. ∀a,b:E. a ≰ b → b < a.
+
+lemma dual_exc: excess→ excess.
+intro E; apply mk_excess; 
+[apply (exc_carr E);|apply (λx,y:E.y≰x);|apply exc_coreflexive;
+|unfold cotransitive; simplify;intros;cases (exc_cotransitive E ??z e);
+  [right|left]assumption]
+qed.