proposition: Lemma BDDcompare_sup_inf : forall x y : BDDvar, BDDcompare x y = Datatypes.Gt -> BDDcompare y x = Datatypes.Lt.
proof: Proof. double induction x y. simpl in |- *. intro; discriminate. simpl in |- *. intro p. intro; discriminate. simpl in |- *. reflexivity. unfold BDDcompare in |- *. intros p p0 H. apply ZC1. assumption. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps)