proposition: Lemma BDDvar_le_max_2 : forall x y : BDDvar, BDDvar_le x (BDDvar_max y x) = true.
proof: Proof. unfold BDDvar_max in |- *. unfold BDDvar_le in |- *. intros x y. elim (sumbool_of_bool (Nleb y x)). intro y0. rewrite y0. apply Nleb_refl. intro y0. rewrite y0. apply Nltb_leb_weak. assumption. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2 bdd3 bdd4 bdd5_1 bdd5_2 bdd6