proposition: Theorem wf_lexprod : well_founded leA -> (forall x : A, well_founded (leB x)) -> well_founded LexProd.
proof: Proof. intros wfA wfB; unfold well_founded. destruct a. apply acc_A_B_lexprod; auto with sets; intros. red in wfB. auto with sets. Defined.
imports: EqdepFacts Relation_Operators Transitive_Closure Inclusion Inverse_Image