proposition: Lemma inj_mul x y : 0 < x -> 0 < y -> Z.to_pos (x*y) = (Z.to_pos x * Z.to_pos y)%positive.
proof: Proof. destruct x; easy || now destruct y. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass