proposition: Lemma inj_min (n m : nat) : Pos.of_nat (min n m) = Pos.min (Pos.of_nat n) (Pos.of_nat m).
proof: Proof. destruct n as [|n]. { simpl. symmetry. apply Pos.min_l, Pos.le_1_l. } destruct m as [|m]. { simpl. symmetry. apply Pos.min_r, Pos.le_1_l. } unfold Pos.min. rewrite <- inj_compare by easy. case Nat.compare_spec; intros H; f_equal; apply Nat.min_l || apply Nat.min_r. - rewrite H; auto. - now apply Nat.lt_le_incl. - now apply Nat.lt_le_incl. Qed.
imports: BinPos PeanoNat