proposition: Lemma congrrule_sym u v : v \in congrrule u -> u \in congrrule v.
proof: Proof. Proof using Hsym. move/flatten_mapP => [[[i j1] k]]. rewrite -cat3_equiv_cut3 /= => /eqP -> /mapP[j2 /Hsym Hj2 ->]. by apply: congrrule_is_congr; exact: rule_congrrule. Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK