proposition: Lemma square_plus3_square m n: n ^2 + 3 = m ^2 -> (n = 1 /\ m = 2).
proof: Proof. move => eq1. move:(subn_sqr m n); rewrite -eq1 addKn. case: (ltnP m n); first by rewrite -ltn_sqr - (addn0 (n^2)) -eq1 ltn_add2l. move => ha; rewrite -{2 3} (subnK ha)- addnA addnn => eqB. have: (m-n) < 2 by rewrite - ltn_sqr ltnS eqB mulnDr mulnn leq_addr. move: eqB;case: (m-n) => //; case => // /eqP. by rewrite mul1n -[3]/(1+1.*2) (eqn_add2l) eqn_double => /eqP <-. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)