proposition: Theorem div2_rem2_eq : forall n, 2 * div2 n + rem2 n = n.
proof: Proof. intros n; elim n using div2_ind; try (simpl; auto with arith; fail). intros p IHp; pattern p at 3; rewrite <- IHp. simpl;ring. Qed.
imports: Arith ArithRing