proposition: Lemma Zrem_odd : forall a, Z.rem a 2 = if Z.odd a then Z.sgn a else 0.
proof: Proof. intros. symmetry. apply Zrem_unique_full with (Z.quot2 a). - apply Zquot2_odd_remainder. - apply Zquot2_odd_eqn. Qed.
imports: Nnat ZArith_base Lia ZArithRing Zdiv Morphisms