proposition: Lemma Zmax_or_informative : forall n m : Z, {Zmax n m = n} + {Zmax n m = m}.
proof: Proof. intros. unfold Zmax in |- *. case Zmin_or_informative with (n := n) (m := m). intro. rewrite e. right. ring. intro. rewrite e. left. ring. Qed.
imports: Coq(Lia)