proposition: Lemma lt_max_nat_of_N : forall x y z : BDDvar, BDDcompare (BDDvar_max x y) z = Datatypes.Lt -> max (nat_of_N x) (nat_of_N y) < nat_of_N z.
proof: Proof. unfold BDDvar_max in |- *. unfold BDDvar_le in |- *. intros x y z. elim (sumbool_of_bool (Nleb x y)). intro y0. rewrite y0. intro H. unfold max in |- *. elim (sumbool_of_bool (leb (nat_of_N x) (nat_of_N y))). intro y1. rewrite y1. apply BDDcompare_lt. assumption. intro y1. rewrite y1. apply le_lt_trans with (m := nat_of_N y). apply leb_complete. exact y0. apply BDDcompare_lt. assumption. intro y0. rewrite y0. intro H. unfold max in |- *. elim (sumbool_of_bool (leb (nat_of_N x) (nat_of_N y))). intro y1. cut (Nleb x y = true). intro H0. rewrite H0 in y0. discriminate. exact y1. intro y1. rewrite y1. 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