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