proposition: Theorem le_max_l : ∀ n m, n ≤ max n m.
proof: Proof. intros n m. destruct n as [n| ]; [ idtac | constructor ]. destruct m as [m| ]; [ simpl | constructor ]. apply fin_le_mono, Nat.le_max_l. Qed.
imports: Utf8 Compare_dec NPeano Misc