proposition: Lemma max_lt_r : forall x y z, x <= z -> x <= max y z.
proof: Proof. induction x. auto with arith. induction y. auto with arith. simpl. induction z. lia. auto with arith. Qed.
imports: Coq.Arith.Arith Coq.Arith.Max Coq.Classes.EquivDec Coq.Lists.List Coq.Structures.Equalities Coq.FSets.FSets Metalib.CoqListFacts Metalib.FSetExtra Metalib.FSetWeakNotin Metalib.LibTactics Lia