proposition: Lemma Zle_max_l : forall n m : Z, (n <= Zmax n m)%Z.
proof: Proof. intros. unfold Zmax in |- *. apply Zplus_le_reg_l with (p := (- n + Z.min n m)%Z). ring_simplify (- n + Z.min n m + n)%Z. ring_simplify (- n + Z.min n m + (n + m - Z.min n m))%Z. apply Z.le_min_r. Qed.
imports: Coq(Lia)