proposition: Lemma suspend_bound_gset S x (Sg: gset S) (bound: g S x): gset (suspend S x).
proof: Proof. split. split. - intros y z [iny|iny] [inz|inz]. + apply (wo_total S); auto using C_wo. + rewrite <- inz; left. apply ltA_spec, (upper_bound S); auto using C_wo. + rewrite <- iny; right. apply ltA_spec, (upper_bound S); auto using C_wo. + now rewrite <- iny, <- inz; left. - intros Y Ysub inh. destruct (classic (inhabited (restrict x Y))) as [case|case]. + destruct (wo_minima S Sg (restrict x Y)) as [m [[inm neq] bound']]; auto. * intros z [[inz|eqz]%Ysub ltz]; auto. rewrite eqz in ltz; apply irreflexivity in ltz; contradiction. * exists m; split; trivial. intros z inz. destruct (classic (z ≺ x)) as [case'|case']; [apply bound'; split; trivial|]. apply Ysub in inz. apply ltA_spec. destruct inz as [inz|<-]; trivial. now eapply upper_bound in inz; eauto using C_wo. + assert (∀ y, y ∈ Y ↔ x ≌ y). { split. - intro iny. unfold restrict, inhabited in case; cbn in case. assert (¬y ≺ x) as bound' by firstorder. apply Ysub in iny; destruct iny as [iny|]; trivial. now eapply upper_bound in iny; eauto using C_wo. - intros <-. destruct inh as [z inz]. destruct (classic (x ∈ Y)) as [|notinx]; trivial. contradict case; exists z. split; trivial. eapply upper_bound; eauto using C_wo. destruct (Ysub _ inz) as [|eqy]; trivial. now rewrite eqy in notinx. } setoid_rewrite H. exists x; split; [|intros ? <-]; reflexivity. - intros c inc. assert (restrict c (suspend S x) ≌ restrict c S) as ->. + apply subset_equ. * intros y [[iny|<-] lty]; [split; trivial|]. apply (lt_le_trans _ _ ltA_spec x c x), irreflexivity in lty; [contradiction|]. destruct inc as [inc| ->]; [|reflexivity]. eapply ltA_spec, upper_bound; eauto using C_wo. * intros y [iny bound']; split; trivial. left; trivial. + destruct inc as [inc|<-]; trivial. * apply C_bounds; trivial. * enough (restrict x S ≌ S) as -> by trivial. apply subset_equ; [destruct 1; trivial|]. intros y iny; split; trivial. eapply upper_bound; eauto using C_wo. Qed.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)