proposition: Lemma rt_clot_S_S n (M: bmx (1+n)%nat (1+n)%nat): forall i j, rt_clot (sub11_mx M) i j -> rt_clot M (rshift i) (rshift j).
proof: Proof. induction 1. constructor. eapply clot_cons; eassumption. Qed.
imports: kleene boolean sups matrix