proposition: Lemma tst_dotA: forall a b c : test, a·(b·c) ≡ (a·b)·c.
proof: Proof. intros [a] [b] [c]. apply dotA. Qed.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries setoid_bigop structures)