proposition: Lemma cycTI_NC_add n1 n2 phi1 phi2 : (NC phi1 <= n1 -> NC phi2 <= n2 -> NC (phi1 + phi2)%R <= n1 + n2)%N.
proof: Proof. move=> ub1 ub2; apply: leq_trans {ub1 ub2}(leq_add ub1 ub2). rewrite -cardsUI -[NC _]addn0 leq_add // subset_leq_card //. apply/subsetP=> [[i j]]; rewrite !inE /= -negb_and cfdotDl. by apply: contra => /andP[/eqP-> /eqP->]; rewrite addr0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg matrix poly finset) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor center gproduct cyclic pgroup abelian frobenius) mathcomp(mxalgebra mxrepresentation vector falgebra fieldext galois) mathcomp(ssrnum rat algC algnum classfun character) mathcomp(integral_char inertia vcharacter) odd_order(PFsection1 PFsection2)