proposition: Lemma mx_point_plus: forall n m i j (a b: X A A), mx_point n m i j a + mx_point n m i j b == mx_point n m i j (a+b).
proof: Proof. repeat intro. simpl. nat_analyse; trivial with algebra. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(MxGraph) ATBR(SemiLattice) ATBR(BoolView)