-#n #len #notB >eq_B_B1 >eq_B1_times_B_split1_B_split2 @le_times
- [@(transitive_le ? (teta ((2*n)/3)))
- [@le_B_split1_teta [@(transitive_le … len) @leb_true_to_le //|//]
- |@le_teta
+#n #len #notB >eq_B_Bk >eq_Bk_B1_B2 @le_times
+ [@(transitive_le ? (theta ((2*n)/3)))
+ [@le_B1_theta [@(transitive_le … len) @leb_true_to_le //|//]
+ |@le_theta