proposition: Lemma context_big_enough P T (b : big_rel_of T) i s : leq_big_internal b i (bigger_than b s) -> P true -> P (leq_big b i (bigger_than b s)).
proof: Proof. by rewrite leq_big_internalE => ->. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype)