proposition: Lemma well_founded_irreflexive {A} {R : relation A}{wfR : WellFounded R} : forall x y : A, R x y -> x = y -> False.
proof: Proof. intros x y Ryy ->. red in wfR. induction (wfR y) as [y accy IHy]. apply (IHy _ Ryy Ryy). Qed.
imports: Coq(Wf_nat Relations) Coq(Wellfounded Relation_Definitions) Coq(Relation_Operators Lexicographic_Product Wf_nat) Equations(Init Signature) Equations.CoreTactics Equations.Prop.Classes Equations.Prop.EqDec Equations.Prop.DepElim Equations.Prop.Constants