proposition: Lemma big_ord1_cond R idx (op : @Monoid.law R idx) P F : \big[op/idx]_(i < 1 | P i) F i = if P 0 then F 0 else idx.
proof: Proof. by rewrite big_mkcond big_ord1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool choice eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup) mathcomp(ssralg finalg countalg)