proposition: Lemma F_wf_solve_dec2 : forall wpb lpb', o_lpb ((wf_solve wpb) ++ lpb') (wpb :: lpb').
proof: Proof. intros wpb lpb'; unfold o_lpb, wf_solve; destruct wpb. simpl; rewrite map_app; rewrite weight_is_weight. apply (@NatMul.rmv_case lt ((map pb_weight (solve pb)) ++ map wfpb_weight lpb') (pb_weight pb :: map wfpb_weight lpb') (map wfpb_weight lpb') (map pb_weight (solve pb)) (pb_weight pb)). generalize (well_founded_solve pb w). replace (WFMatching.Matching.solve pb) with (solve pb); [idtac | trivial]. clear w lpb'; generalize (solve pb); induction l. contradiction. intros H b In_b; elim In_b; clear In_b; intro In_b. unfold NatMul.LP.EDS.eq_A, NatMul.DS.eq_A in *; subst b; apply H; left; trivial. apply IHl; trivial; intros; apply H; right; trivial. apply NatMul.LP.permut_refl. apply NatMul.LP.permut_refl. Qed.
imports: Coq(Arith List Wellfounded Wf_nat) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory ac matching dickson matching_well_formed matching_well_founded matching_sound matching_complete dickson)