proposition: Lemma BDDcompare_trans : forall x y z : BDDvar, BDDcompare x y = Datatypes.Lt -> BDDcompare y z = Datatypes.Lt -> BDDcompare x z = Datatypes.Lt.
proof: Proof. double induction x y. simpl in |- *. intros z H H0. discriminate H. simpl in |- *. intro p. simple induction z. intros H H0. discriminate H0. trivial. simpl in |- *. intros p z H H0. discriminate H. intro p. intro p0. simple induction z. simpl in |- *. trivial. intro p1. simpl in |- *. intros H H0. cut (nat_of_P p0 < nat_of_P p). cut (nat_of_P p < nat_of_P p1). intros H1 H2. apply nat_of_P_lt_Lt_compare_complement_morphism. apply lt_trans with (m := nat_of_P p). assumption. assumption. apply nat_of_P_lt_Lt_compare_morphism. assumption. apply nat_of_P_lt_Lt_compare_morphism. assumption. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps)