proposition: Theorem div_bin_eq : forall n m:positive, Zpos n = (fst (div_bin n m))*(Zpos m) + snd (div_bin n m).
proof: Proof. intros n m; div_bin_tac n m; rewrite Zpos_xI || (try rewrite Zpos_xO); try rewrite Hrec; unfold fst, snd; ring. Qed.
imports: ZArith List Arith Lia Zwf Program