proposition: Lemma Lt_connect : forall a b, Lt a b \/ a = b \/ Lt b a.
proof: Proof. intros a b ; generalize (well_order (Couple a b) a ). destruct 1 as [ c H1]. - left. - destruct H1 as [H2 H3]. destruct H2. + destruct (H3 b);auto; now right. + destruct (H3 a);auto; now left. Qed.
imports: Coq(Relations Classical Classical_sets RelationClasses Wf_nat) hydras(PartialFun)