proposition: Lemma conv_zero A B: zero B A` == 0.
proof: Proof. transitivity ((dot B A A 0 (0`))`). switch. symmetry. apply dot_ann_left_c. autorewrite with converse_down. apply dot_ann_left_c. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(SemiLattice) ATBR(SemiRing)