proposition: Lemma inj_max a a' : N.to_nat (N.max a a') = Nat.max (N.to_nat a) (N.to_nat a').
proof: Proof. unfold N.max. rewrite inj_compare; symmetry. case Nat.compare_spec; intros. - now apply Nat.max_r, Nat.eq_le_incl. - now apply Nat.max_r, Nat.lt_le_incl. - now apply Nat.max_l, Nat.lt_le_incl. Qed.
imports: BinPos BinNat PeanoNat Pnat