proposition: Lemma ltrXn2r n x y : 0 <= x -> x < y -> x ^+ n < y ^+ n = (n != 0).
proof: Proof. move=> xge0 xlty; case: n; first by rewrite ltxx. elim=> [|n IHn]; rewrite ?[_ ^+ _.+2]exprS //. rewrite (@le_lt_trans _ _ (x * y ^+ n.+1)) ?ler_wpM2l ?ltr_pM2r ?IHn //. by rewrite ltW. by rewrite exprn_gt0 // (le_lt_trans xge0). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)