proposition: Lemma Zquot2_odd_remainder : forall a, Remainder a 2 (if Z.odd a then Z.sgn a else 0).
proof: Proof. intros [ |p|p]. - simpl. left. simpl. auto with zarith. - left. destruct p; simpl; lia. - right. destruct p; simpl; split; now auto with zarith. Qed.
imports: Nnat ZArith_base Lia ZArithRing Zdiv Morphisms