proposition: Lemma par_nontest u v a b c d of is_test a & is_test b & is_test c & is_test d : a·u·b∥c·v·d ≡ (a·c)·(u∥v)·(b·d).
proof: Proof. by rewrite -partst -[a·u·b]dotA -tstpar parC -tstpar -partst !dotA parC. Qed.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries setoid_bigop structures)