proposition: Lemma mx_blocks_leq x y n m: forall (a a': MX x y) b b' c c' (d d': MX n m), mx_blocks a b c d <== mx_blocks a' b' c' d' -> a<==a' /\ b<==b' /\ c<==c' /\ d<==d'.
proof: Proof. unfold leq. intros. apply mx_blocks_equal. rewrite <- mx_blocks_plus. assumption. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(MxGraph) ATBR(SemiLattice) ATBR(BoolView)