proposition: Lemma expR_ge0 x : 0 <= x -> forall n : nat, 0 <= x ^ n.
proof: Proof. move=> x_pos; elim => [// | n IH]. by rewrite -(mulR0 0); apply leR_pmul => //; apply/RleP; rewrite Order.POrderTheory.lexx. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)