proposition: Lemma INFERIEUR_neq_O : forall x y : ad, BDDcompare x y = Datatypes.Lt -> y <> N0.
proof: Proof. double induction x y. simpl in |- *. intro; discriminate. unfold not in |- *; intros. discriminate. simpl in |- *. intros; discriminate. unfold not in |- *; intros. discriminate. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps)