proposition: Lemma BDDcompare_z_nz : forall x : BDDvar, x <> N0 -> BDDcompare N0 x = Datatypes.Lt.
proof: Proof. simple induction x. intros H. absurd (N0 = N0). assumption. reflexivity. simpl in |- *. reflexivity. 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