proposition: Lemma odd_spec n : odd n = true <-> Odd n.
proof: Proof. split. - exists (div2 n). destruct n as [|[ | | ]|[ | | ]]; simpl; try easy. now rewrite Pos.pred_double_succ. - intros (m,->). now destruct m as [|[ | | ]|[ | | ]]. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass