proposition: Lemma mx_point_zero: forall n m i j, 0 == mx_point n m i j (0: X A A).
proof: Proof. repeat intro. simpl. nat_analyse; reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(MxGraph) ATBR(SemiLattice) ATBR(BoolView)