proposition: Lemma BDDcompare_lt : forall x y : BDDvar, BDDcompare x y = Datatypes.Lt -> nat_of_N x < nat_of_N y.
proof: Proof. double induction x y. simpl in |- *. intro H. discriminate. simpl in |- *. intros p H. cut (exists h : nat, nat_of_P p = S h). intro H0. inversion H0. rewrite H1. apply lt_O_Sn. apply ZL4. simpl in |- *. intros p H. discriminate. simpl in |- *. intros p p0 H. apply nat_of_P_lt_Lt_compare_morphism. assumption. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps)