proposition: Lemma BQ_square_2 x : ratp x -> BQsquare x = \2q -> False.
proof: Proof. move => xq; move /(BQ_square_Z xq) => [_ eq1 _]. move: eq1; rewrite BZprodE /BZprod_int; Ytac0; move /pr1_def. move /BQ_P:xq => [_ /BZ_valN nn _ _ ]. case: (equal_or_not (P (P x)) \0c) => qa;first by rewrite qa cprod0l;fprops. case: (equal_or_not (P (P x)) \1c) => qb;first by rewrite qb cprod1l;fprops. move:(cge2 (CS_nat nn) qa qb) clt_24 => qc lt1 eq1. by move: (cprod_Mlele qc qc); rewrite eq1 cprod_22 => /(cltNge lt1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)