proposition: Lemma suspend_good S R x (x_not_in: ¬S x): ordered_subset S R → ordered_subset (suspend_S S x) (suspend_R S R x).
proof: Proof. intros [sproper strict wf proper correct complete]. unfold suspend_S, suspend_R. split. 2:split. - solve_proper. - intros y [[ ]%irreflexivity|[iny eqz]]. now rewrite <- eqz in iny. - intros a b c [ltab|[ina eqb]] [ltbc|[inb eqc]]. + left; transitivity b; trivial. + right; split; trivial. apply correct in ltab; tauto. + apply correct in ltbc. rewrite <- eqb in ltbc; tauto. + auto. - assert (∀ y, ¬eqA x y → Acc (λ y z, R y z ∨ S y ∧ eqA x z) y). + induction y as [y IH] using (well_founded_ind wf). intro neq; constructor; intros z [ltz|[inz eqy]]; [|contradiction]. apply IH; trivial. apply correct in ltz. intro contra; rewrite <- contra in ltz; tauto. + intro y. destruct (classic (eqA x y)) as [eqxy|neq]; auto. constructor. intros z [ltz|[inz eqy]]. * apply H. intro contra; rewrite <- contra, eqxy in ltz. apply irreflexivity in ltz; contradiction. * apply H. now intro contra; rewrite contra in x_not_in. - solve_proper. - intros y z [relyz|[iny eqxz]]; [|tauto]. apply correct in relyz; tauto. - intros y z [iny|eqy] [inz|eqz]; auto. + destruct (complete y z) as [?|[?|?]]; auto. + rewrite <- eqz, eqy; auto. now left. Qed.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)