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