proposition: Lemma inj_max p q : to_nat (max p q) = Nat.max (to_nat p) (to_nat q).
proof: Proof. unfold max. rewrite inj_compare. case Nat.compare_spec; intros H; symmetry. - apply Nat.max_r. now rewrite H. - now apply Nat.max_r, Nat.lt_le_incl. - now apply Nat.max_l, Nat.lt_le_incl. Qed.
imports: BinPos PeanoNat