proposition: Lemma mx_point_scal: forall (a: X A A), mx_point 1 1 0 0 a == mx_of_scal a.
proof: Proof. intro. mx_intros i j Hi Hj. reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(MxGraph) ATBR(SemiLattice) ATBR(BoolView)