proposition: Lemma blk_mx_0 `{laws} u n1 n2 m1 m2 a b c d: @blk_mx (X u u) n1 n2 m1 m2 a b c d ≡ 0 -> a ≡0 /\ b ≡0 /\ c ≡0 /\ d ≡0.
proof: Proof. intro Z. split; [|split; [|split]]. rewrite <-(mx_sub00_blk a b c d). intros ? ?. apply Z. rewrite <-(mx_sub01_blk a b c d). intros ? ?. apply Z. rewrite <-(mx_sub10_blk a b c d). intros ? ?. apply Z. rewrite <-(mx_sub11_blk a b c d). intros ? ?. apply Z. Qed.
imports: kleene normalisation ordinal sups matrix