proposition: Lemma sqrnD_sub m n : n <= m -> (m + n) ^ 2 - 4 * (m * n) = (m - n) ^ 2.
proof: Proof. move=> le_nm; rewrite -[4]/(2 * 2) -mulnA mul2n -addnn subnDA. by rewrite sqrnD addnK sqrnB. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring