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