proposition: Lemma BQ_nat_square_monotone n (x := BQ_of_nat n) : natp n -> x <=q BQsquare x.
proof: Proof. move => nN. have nz:= (BZ_of_nat_i nN). have nzp := (BZ_of_natp_i nN). rewrite /BQ_of_nat/BQsquare (BQprod_cZ nz nz). apply/ (qle_cZ nz (ZSp nz nz)). rewrite (BZprod_cN nN nN); apply/(zle_cN nN (NS_prod nN nN)). case: (equal_or_not n \0c) => enz; first by rewrite enz; apply:cle0x; fprops. exact:(cprod_M1le (CS_nat nN) enz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)