proposition: Lemma clot_snoc n (M: bmx n n): forall i j k, rt_clot M i j -> M j k -> rt_clot M i k.
proof: Proof. intros. eapply clot_app. eassumption. eapply clot_cons. eassumption. constructor. Qed.
imports: kleene boolean sups matrix