proposition: Theorem max_l : ∀ n m, m ≤ n → max n m = n.
proof: Proof. intros n m H. destruct n as [n| ]; [ simpl | destruct m; reflexivity ]. destruct m as [m| ]; [ idtac | inversion H ]. rewrite Nat.max_l; [ reflexivity | inversion H; assumption ]. Qed.
imports: Utf8 Compare_dec NPeano Misc