proposition: Lemma Zmax_case : forall (n m : Z) (P : Z -> Type), P n -> P m -> P (Zmax n m).
proof: Proof. intros. unfold Zmax in |- *. case Zmin_or_informative with (n := n) (m := m). intro. rewrite e. cut ((n + m - n)%Z = m). intro. rewrite H. assumption. ring. intro. rewrite e. cut ((n + m - m)%Z = n). intro. rewrite H. assumption. ring. Qed.
imports: Coq(Lia)