proposition: Lemma inj_min p q : to_nat (min p q) = Nat.min (to_nat p) (to_nat q).
proof: Proof. unfold min. rewrite inj_compare. case Nat.compare_spec; intros H; symmetry. - apply Nat.min_l. now rewrite H. - now apply Nat.min_l, Nat.lt_le_incl. - now apply Nat.min_r, Nat.lt_le_incl. Qed.
imports: BinPos PeanoNat