proposition: Lemma size_prop1 a b c n d (l:= size (cons a b c n d)): [&& size a < l, size b < l, size c < l, size d < l & size [a, b, c] <= l]%N.
proof: Proof. by rewrite size_a size_b size_c size_d size_psi. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)