proposition: Lemma onemX_NngNum r (r1 : r <= 1) (r0 : 0 <= r) n : `1-(r ^+ n) = (NngNum (onemX_ge0 n r0 r1))%:num.
proof: Proof. by []. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)