proposition: Lemma par_test a u of is_test a : is_test (a∥u).
proof: Proof. constructor; apply/is_test_alt. by rewrite -parA (parC u) parA tstpar1. Qed.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries setoid_bigop structures)