proposition: Lemma BDDvar_max_lemma_1 : forall x y z : BDDvar, BDDcompare x y = Datatypes.Lt -> BDDcompare (BDDvar_max x N0) (BDDvar_max y z) = Datatypes.Lt.
proof: Proof. intros x y z. rewrite (BDDvar_max_comm x N0). unfold BDDvar_max in |- *. simpl in |- *. intro H. unfold BDDvar_le in |- *. unfold Nleb in |- *. elim (sumbool_of_bool (leb (nat_of_N y) (nat_of_N z))). intro y0. rewrite y0. apply BDDlt_compare. apply lt_le_trans with (m := nat_of_N y). apply BDDcompare_lt. assumption. apply leb_complete. assumption. intro y0. rewrite y0. 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