proposition: Lemma Zquot2_quot n : Z.quot2 n = n ÷ 2.
proof: Proof. assert (AUX : forall m, 0 < m -> Z.quot2 m = m ÷ 2). { intros m Hm. apply Z.quot_unique with (if Z.odd m then Z.sgn m else 0). - now apply Z.lt_le_incl. - rewrite Z.sgn_pos by trivial. destruct (Z.odd m); now split. - apply Zquot2_odd_eqn. } destruct (Z.lt_trichotomy 0 n) as [POS|[NUL|NEG]]. - now apply AUX. - now subst. - apply Z.opp_inj. rewrite <- Z.quot_opp_l, <- Zquot2_opp. + apply AUX. now destruct n. + easy. Qed.
imports: BinInt