proposition: Lemma wf_from_wqo : forall (X:Type) (R : X -> X -> Prop), transitive X R -> almost_full R -> well_founded (fun x y => R x y /\ ~ R y x).
proof: Proof. intros X R trH afR. apply wf_from_af with (R := R). intros. destruct H. assert (~ R y x). induction H. destruct H; auto. destruct H. assert (R z y). eapply trH. apply H0. apply H. assert (~ R z y). apply IHclos_trans_1n. assumption. firstorder. firstorder. assumption. Defined.
imports: Coq(Arith Relations)