proposition: Lemma wBwB_lex: forall a b c d, a * wB^2 + [[b]] <= c * wB^2 + [[d]] -> a <= c.
proof: Proof. intros a b c d H; apply beta_lex with [[b]] [[d]] (wB^2);zarith. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase