proposition: Lemma egality_case_sum_of_four : forall a b c d M, a <= M -> b <= M -> c <= M -> d <= M -> a + b + c + d = 4 * M -> ((a = M) /\ (b = M)) /\ ((c = M) /\ (d = M)).
proof: Proof. intros. lia. Qed.
imports: ZArith Lia Znumtheory Natsets MyNat Ztools Zeqm Znumfacts