proposition: Theorem bmx_str_clot n (M: bmx n n) i j: M^* i j <-> rt_clot M i j.
proof: Proof. split. - assert (M^* i j ≡ bmx_str M i j). apply bmx_str_str. rewrite H. clear H. revert i j. induction n as [|n IH]; intros i' j'. simpl. intro. eapply clot_cons. eassumption. constructor. unfold bmx_str; fold (@bmx_str n). set (M' := sub11_mx (n1:=1) (m1:=1) M). specialize (IH M'). unfold blk_mx, row_mx, col_mx. case ordinal.split_spec; intros i ->; case ordinal.split_spec; intros j -> Hij. + setoid_rewrite ord0_unique. constructor. + setoid_rewrite is_true_sup in Hij. destruct Hij as [k [_ Hk]]. apply Bool.andb_true_iff in Hk as [Hik Hkj]. apply IH in Hkj. unfold M' in Hkj. eapply clot_cons. eassumption. now apply rt_clot_S_S. + setoid_rewrite is_true_sup in Hij. destruct Hij as [k [_ Hk]]. apply Bool.andb_true_iff in Hk as [Hik Hkj]. apply IH in Hik. unfold M' in Hik. eapply clot_snoc. apply rt_clot_S_S; eassumption. assumption. + setoid_rewrite Bool.orb_true_iff in Hij. destruct Hij as [Hij|Hij]. apply IH in Hij. now apply rt_clot_S_S. setoid_rewrite is_true_sup in Hij. destruct Hij as [k [_ Hk]]. apply Bool.andb_true_iff in Hk as [Hik Hkj]. setoid_rewrite is_true_sup in Hik. destruct Hik as [i' [_ Hi']]. apply Bool.andb_true_iff in Hi' as [Hii' Hi'k]. setoid_rewrite is_true_sup in Hkj. destruct Hkj as [j' [_ Hj']]. apply Bool.andb_true_iff in Hj' as [Hkj' Hj'j]. apply IH in Hii'. apply IH in Hj'j. eapply clot_app. apply rt_clot_S_S, Hii'. eapply clot_cons. apply Hi'k. eapply clot_cons. apply Hkj'. apply rt_clot_S_S, Hj'j. - induction 1 as [i|i j k Hij Hjk IH]. + pose proof (str_refl (X:=bmx) M i i). simpl in H. apply H. unfold mx_one. now rewrite eqb_refl. + pose proof (str_cons (X:=bmx) M i k). simpl in H. apply H. clear H. unfold mx_dot. rewrite is_true_sup. eexists. split. apply in_seq. apply Bool.andb_true_iff. split; eassumption. Qed.
imports: kleene boolean sups matrix