Lemma max_le_l : ∏ n m : nat, (n ≤ max n m)%nat. Proof. induction n as [ | n IHn] ; simpl max. - intros m ; reflexivity. - induction m as [ | m _]. + now apply isreflnatleh. + now apply IHn. Qed.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Subtypes.