proposition: Lemma steps_least: forall j, steps i j -> exists w, w ≦ vars A /\ j = Ms i w.
proof: Proof. intros j H. apply bmx_str_clot in H. induction H as [i|i j k Hij _ [w [Hw ->]]]. exists nil. split. lattice. reflexivity. setoid_rewrite is_true_sup in Hij. destruct Hij as [a [Ha Hij]]. exists (a::w). split. intros b [<-|Hb]. assumption. now apply Hw. revert Hij. case eqb_ord_spec. 2: discriminate. now intros <-. Qed.
imports: comparisons positives ordinal pair lset monoid boolean prop sups bmx