proposition: Lemma instantiate_bigger_than T (b : big_rel_of T) i s : leq_big_internal b i (bigger_than b (i :: s)).
proof: Proof. by case: b i s => [? []]. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype)