proposition: Lemma increase_bound : forall (bs : BDDstate) (n n' : BDDvar) (node : ad), BDDbounded bs node n -> BDDcompare n n' = Datatypes.Lt -> BDDbounded bs node n'.
proof: Proof. intro bs. intro n. intro n'. intro node. intro H. elim H. intros n0 H0. apply BDDbounded_0. intros n0 H0. apply BDDbounded_1. intros node0 n0 x l r H0 H1 H2 H3 H4 H5 H6 H7. apply BDDbounded_2 with (x := x) (l := l) (r := r). assumption. apply BDDcompare_trans with (y := n0). assumption. assumption. assumption. assumption. assumption. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat