proposition: Lemma max_le_r : ∏ n m : nat, (m ≤ max n m)%nat.
proof: Proof. induction n as [ | n IHn] ; simpl max. - intros m ; now apply isreflnatleh. - induction m as [ | m _]. + reflexivity. + now apply IHn. Qed.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Combinatorics.FiniteSequences UniMath.Foundations.NaturalNumbers UniMath.Tactics.EnsureStructuredProofs