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