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