proposition: Lemma mx_to_scal_plus: forall a b: MX 1 1, mx_to_scal a + mx_to_scal b == mx_to_scal (a+b).
proof: Proof. reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(MxGraph) ATBR(SemiLattice) ATBR(BoolView)