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