proposition: Lemma BDDvar_max_comm : forall x y : BDDvar, BDDvar_max x y = BDDvar_max y x.
proof: Proof. unfold BDDvar_max in |- *. unfold BDDvar_le in |- *. intros x y. elim (sumbool_of_bool (Nleb x y)). intro y0. rewrite y0. elim (sumbool_of_bool (Nleb y x)). intro y1. rewrite y1. apply Nleb_antisym. assumption. assumption. intro y1. rewrite y1. reflexivity. intro y0. rewrite y0. elim (sumbool_of_bool (Nleb y x)). intro y1. rewrite y1. reflexivity. intro y1. rewrite y1. apply Nleb_antisym. apply Nltb_leb_weak. assumption. apply Nltb_leb_weak. 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