proposition: Lemma le_nat_of_N_max : forall x y z : BDDvar, BDDvar_le x (BDDvar_max y z) = true -> nat_of_N x <= max (nat_of_N y) (nat_of_N z).
proof: Proof. unfold BDDvar_max in |- *. unfold BDDvar_le in |- *. intros x y z. elim (sumbool_of_bool (Nleb y z)). intro y0. rewrite y0. intro H. unfold max in |- *. elim (sumbool_of_bool (leb (nat_of_N y) (nat_of_N z))). intro y1. rewrite y1. apply leb_complete. assumption. unfold Nleb in y0. rewrite y0. intro y1. discriminate. intro y0. rewrite y0. intro H. unfold max in |- *. unfold Nleb in y0, H. rewrite y0. apply leb_complete. 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