proposition: Lemma BDDcompare_1 : forall x y : BDDvar, BDDcompare x y = Datatypes.Lt -> BDDcompare (ad_S x) y = Datatypes.Lt \/ ad_S x = y.
proof: Proof. intros x y H. elim (relation_sum (BDDcompare (ad_S x) y)). intro y0. elim y0; intro. right. apply BDD_EGAL_complete. assumption. left; assumption. intro y0. absurd (nat_of_N x < nat_of_N x). apply lt_irrefl. apply lt_trans_1 with (y := nat_of_N y). apply BDDcompare_lt. assumption. rewrite <- (ad_S_is_S x). apply BDDcompare_lt. apply BDDcompare_sup_inf. assumption. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps)