proposition: Lemma nat_Cauchy m n : 2 * (m * n) <= m ^ 2 + n ^ 2 ?= iff (m == n).
proof: Proof. without loss le_nm: m n / n <= m. by have [?|/ltnW ?] := leqP n m; last rewrite eq_sym addnC (mulnC m); apply. apply/leqifP; have [-> | ne_mn] := eqVneq; first by rewrite addnn mul2n. by rewrite -subn_gt0 -sqrnB // sqrn_gt0 subn_gt0 ltn_neqAle eq_sym ne_mn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring