proposition: Lemma A14_ (x y z: A): dom x·(y∥z) ≡ dom x·y ∥ z.
proof: Proof. by rewrite domE parC A12 (A12 _ y) parA. Qed.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries setoid_bigop structures pttdom)