proposition: Lemma mx_div_level l : DIV ≪ l -> mx_level l ≪ l -> BDL+DIV ≪ l.
proof: Proof. rewrite 3lower_spec. unfold mx_level. simpl. case (has_div l). simpl. tauto. intuition discriminate. Qed.
imports: comparisons kleene sums normalisation