proposition: Lemma permc_addc (g : edge_perm) c1 c2 : g (c1 +c c2) = g c1 +c g c2.
proof: Proof. by case: g; case: c1; case: c2. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype)