proposition: Lemma BDDcompare_le_INFERIEUR_1 : forall x y z : BDDvar, BDDvar_le x y = true -> BDDcompare y z = Datatypes.Lt -> BDDcompare x z = Datatypes.Lt.
proof: Proof. intros x y z H H0. apply BDDlt_compare. apply le_lt_trans with (m := nat_of_N y). unfold BDDvar_le in H. unfold Nleb in H. apply leb_complete; assumption. apply BDDcompare_lt. assumption. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2 bdd3 bdd4 bdd5_1 bdd5_2