proposition: Lemma mx_sub_plus x y n m n' m': forall M N: MX n' m', mx_sub x y n m M + mx_sub x y n m N == mx_sub x y n m (M+N).
proof: Proof. reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(MxGraph) ATBR(SemiLattice) ATBR(BoolView)