proposition: Lemma inj_succ_double x : 0 < x -> Z.to_pos (Z.succ_double x) = (Z.to_pos x)~1%positive.
proof: Proof. now destruct x. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass