proposition: Lemma big_ord1 (F: 'I_1 -> R): \big[op/idx]_(i < 1) (F i) = F ord0.
proof: Proof. by rewrite big_ord_recl big_ord0 Monoid.mulm1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq choice fintype binomial) mathcomp(bigop ssralg poly ssrint) gaia(ssete7)