proposition: Theorem Rpos_div2_wf : well_founded Rpos_div2.
proof: Proof. unfold well_founded; intros a; elim a; (intros; apply Acc_intro; intros y Hr; inversion Hr; auto). Qed.
imports: ZArith List Arith Lia Zwf Relations Inverse_Image Transitive_Closure