proposition: Lemma one_blk_mx n m: (1: mx (n+m) (n+m)) ≡ blk_mx 1 0 0 1.
proof: Proof. intros i j. unfold blk_mx, col_mx, row_mx. case split_spec; intros [i' Hi] ->; case split_spec; intros [j' Hj] ->. reflexivity. simpl. unfold mx_one. now setoid_rewrite eqb_ord_lrshift. simpl. unfold mx_one. now setoid_rewrite eqb_ord_rlshift. simpl. unfold mx_one. now setoid_rewrite eqb_ord_rrshift. Qed.
imports: comparisons kleene sums normalisation