proposition: Lemma pos_lt_wf : well_founded Pos.lt.
proof: Proof. intros x. assert (H:= wf_inverse_image_transparent _ _ Nat.lt Pos.to_nat lt_wf). assert (H0 : Relation_Definitions.inclusion positive Pos.lt (fun x y : positive => Nat.lt (Pos.to_nat x) (Pos.to_nat y))). - red; intros x0 y0 ; now rewrite Pos2Nat.inj_lt . - apply (wf_incl_transparent positive _ _ H0 H ). Defined.
imports: Coq(Arith NArith Lia Recdef) additions(Pow Compatibility Wf_transparent)