proposition: Theorem wf_lexprod : well_founded leA -> well_founded leB -> well_founded lexprod.
proof: Proof. intros wfA wfB; unfold well_founded. destruct a. apply acc_A_B_lexprod; auto with sets; intros. Defined.
imports: Coq(Wf_nat Relations) Coq(Wellfounded Relation_Definitions) Coq(Relation_Operators Lexicographic_Product Wf_nat) Equations(Init Signature) Equations.CoreTactics Equations.Prop.Classes Equations.Prop.EqDec Equations.Prop.DepElim Equations.Prop.Constants