proposition: Lemma mx_blocks_one x n : 1 == @mx_blocks _ A x x n n 1 0 0 1.
proof: Proof. simpl. intros. destruct_blocks; nat_analyse; reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(BoolView)