proposition: Lemma Zwf_pos : well_founded (fun x y => Zpos x < Zpos y).
proof: Proof. unfold well_founded. assert (forall x a ,x = Zpos a -> Acc (fun x y : positive => x < y) a). intros x;assert (Hacc := Zwf_well_founded 0 x);induction Hacc;intros;subst x. constructor;intros. apply H0 with (Zpos y);trivial. split;auto with zarith. intros a;apply H with (Zpos a);trivial. Qed.
imports: ZArith Lia ZCmisc Zwf