proposition: Lemma noCycle_tree : forall x y : tree, x = y -> nlt x y.
proof: Proof. Proof with trivial. intros x y <-. induction x as [|l Hl r Hr]. * now simpl. * split. { change (nle (node l r) r). revert Hr. generalize r at 2 4 as r'. induction r'; intros Hr. split... intro H; noconf H. split. + intro Heq; noconf Heq. now apply (fst (fst Hr)). + firstorder. } { change (nle (node l r) l). revert Hl. generalize l at 2 4 as l'. induction l'; intros Hl'. split... - now intro H; noconf H. - split. + intro Heq; noconf Heq; firstorder. + firstorder. } Qed.
imports: Equations.Prop.Equations