proposition: Lemma size_prop a b n c a' b' n' c' (l := (size (cons a b n c) + size (cons a' b' n' c'))%N) : (size c + size c' < l)%N /\ (size [a, b] + size b' < l)%N /\ (size a' + size a < l)%N /\ (size b + size b' < l)%N /\ (size b + size [a', b'] < l)%N /\ (size a + size a' < l)%N.
proof: Proof. move: (size_prop1 a b n c) => [pa pb pc pd]. move: (size_prop1 a' b' n' c') => [pa' pb' pc' pd']. rewrite (ltn_add_ll pc pc') (ltn_add_ll pb pb') (ltn_add_el pd pb'). by rewrite (ltn_add_le pb pd') (addnC (size a')) (ltn_add_ll pa pa'). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)