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