proposition: Lemma Zmin_or_informative : forall n m : Z, {Z.min n m = n} + {Z.min n m = m}.
proof: Proof. intros. case (Z_lt_ge_dec n m). unfold Z.min in |- *. unfold Z.lt in |- *. intro z. rewrite z. left. reflexivity. intro. cut ({(n > m)%Z} + {n = m :>Z}). intro. case H. intros z0. unfold Z.min in |- *. unfold Z.gt in z0. rewrite z0. right. reflexivity. intro. rewrite e. right. apply Zmin_n_n. cut ({(m < n)%Z} + {m = n :>Z}). intro. elim H. intro. left. apply Z.lt_gt. assumption. intro. right. symmetry in |- *. assumption. apply Z_le_lt_eq_dec. apply Z.ge_le. assumption. Qed.
imports: Coq(Lia)