proposition: Lemma acc_A_B_lexprod : forall x : A, Acc leA x -> (forall x0 : A, clos_trans A leA x0 x -> well_founded (leB x0)) -> forall y : B x, Acc (leB x) y -> Acc LexProd (x; y).
proof: Proof. induction 1 as [x _ IHAcc]; intros H2 y. induction 1 as [x0 H IHAcc0]; intros. apply Acc_intro. destruct y as [x2 y1]; intro H6. simple inversion H6; intro. - cut (leA x2 x); intros. + apply IHAcc; auto with sets. * intros. apply H2. apply t_trans with x2; auto with sets. * red in H2. apply H2. auto with sets. + injection H1 as [= <- _]. injection H3 as [= <- _]; auto with sets. - rewrite <- H1. apply eq_sigT_eq_dep in H3. destruct H3. apply IHAcc0. assumption. Defined.
imports: EqdepFacts Relation_Operators Transitive_Closure Inclusion Inverse_Image