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