proposition: Lemma Le_antisym : forall a b, Le a b -> Le b a -> a = b.
proof: Proof. intros a b H H'; case H; case H' ; try tauto. - symmetry; tauto. - intros;case (Lt_irreflexive (a:=a)); eapply (Lt_trans );eauto. Qed.
imports: Coq(Relations Classical Classical_sets RelationClasses Wf_nat) hydras(PartialFun)