proposition: Lemma x_x2_max q : q * (1 - q) <= / 4.
proof: Proof. rewrite x_x2_eq. have : forall a b, 0 <= b -> a - b <= a. move=> *; Lra.lra. apply; apply mulR_ge0; [Lra.lra | exact: pow_even_ge0]. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR realType_ext Reals Lra mathcomp(lra)