proposition: Lemma Zodd_quot2_neg n : n <= 0 -> Zodd n -> n = 2 * Z.quot2 n - 1.
proof: Proof. intros Hn Hn'. apply Zodd_bool_iff in Hn'. rewrite (Zquot2_odd_eqn n) at 1; rewrite Hn'. unfold Z.sub. f_equal. destruct n; (now destruct Hn) || easy. Qed.
imports: BinInt