proposition: Lemma decomposition_step_decreases_e : forall pb (Inv_pb : Inv_solved_part pb), lt_exc_pb_ok (decomposition_step_e (OK (Normal _ pb) Inv_pb)) (OK (Normal _ pb) Inv_pb).
proof: Proof. intros pb Inv_pb; rewrite decomposition_e_unfold_normal. unfold lt_exc_pb_ok, lt_weight_exc_pb_ok, lt_pb; simpl. generalize (decomposition_step_decreases pb Inv_pb). destruct (decomposition_step pb). trivial. intros _; generalize (beq_nat_ok 1 2); case (Nat.eqb 1 2); [intros; discriminate | auto with arith]. intros _; generalize (beq_nat_ok 0 2); case (Nat.eqb 0 2); [intros; discriminate | auto with arith]. Defined.
imports: Coq(Arith Wf_nat Wellfounded List Multiset Relations) CoLoR(closure decidable_set ordered_set more_list list_permut list_set list_sort dickson term_spec term)