Require Import Vbase Relations ClassicalDescription ClassicalChoice.
Require Import List Permutation Sorting extralib.
Require Import c11 exps.
Require Import GpsFraction GpsSepAlg GpsModel.

Set Implicit Arguments.

Lemma get_state_lt2 tau (S S': slist tau) (L: slist_lt S S') s (IN: In s (SL_list S)) :
  prot_trans tau s (get_state S').
Proof.
  ins; red in L; apply L in IN; desf; eauto using get_state_lt, prot_trans_trans.
Qed.

Lemma slist_lt_trans A (x y z: slist A) :
  slist_lt x y →
  slist_lt y z →
  slist_lt x z.
Proof.
  unfold slist_lt; ins; desf.
  edestruct H as (? & ? & ?); eauto.
  edestruct H0 as (? & ? & ?); eauto using prot_trans_trans.
Qed.

Lemma slist_ltD tau (S S': slist tau) :
  slist_lt S S' ↔ prot_trans tau (get_state S) (get_state S').
Proof.
  unfold slist_lt; split; ins; desf.
  destruct (H _ (get_state_in _)) as (? & ? & ?); eauto using prot_trans_trans, get_state_lt.
  eauto using prot_trans_trans, get_state_lt, get_state_in.
Qed.

Lemma get_state_eq_incl_helper tau (S S': slist tau) :
  (∀ x, In x (SL_list S) → In x (SL_list S')) →
  slist_lt S' S →
  get_state S = get_state S'.
Proof.
  ins; rewrite slist_ltD in ×.
  eapply (prot_trans_ord tau); eauto using get_state_in, get_state_lt.
Qed.

Lemma get_state_eq_prove :
  ∀ tau s (S : slist tau)
    (IN : In s (SL_list S))
    (LAST : ∀ s0, In s0 (SL_list S) → prot_trans tau s0 s),
  get_state S = s.
Proof.
  unfold get_state; destruct S; ins.
  des_eqrefl.
    exfalso.
  induction SL_list using rev_ind; ins; rewrite rev_app_distr in *; ins.
  induction SL_list using rev_ind; ins; clear IHSL_list.
  rewrite rev_app_distr in *; ins; desf.
  eapply prot_trans_ord; eauto using in_or_app, in_eq.
  rewrite in_app_iff in *; ins; desf; eauto using prot_trans_refl.
  by eapply Sorted_app_end_inv; eauto.
Qed.

Lemma res_get_plus r l tau S r' :
  res_get r l = p_at tau S →
  (res_plus r r') ≠ Rundef →
  ∃ S',
    res_get (res_plus r r') l = p_at tau S' ∧
    ∀ s (SIN: In s (SL_list S)), In s (SL_list S').
Proof.
  destruct r, r'; ins; desf; ins.
  inv_lplus l; rewrite H in ×.
  ins; desf; repeat eexists; eauto.
  intros; eapply In_mk_slist; eauto using in_or_app.
Qed.

Lemma res_get_plus2 r l tau S r' S' :
  res_get r l = p_at tau S →
  res_get r' l = p_at tau S' →
  (res_plus r r') ≠ Rundef →
  ∃ S'',
    res_get (res_plus r r') l = p_at tau S'' ∧
    ∀ s, In s (SL_list S'') ↔ In s (SL_list S) ∨ In s (SL_list S').
Proof.
  destruct r, r'; ins; desf; ins.
  inv_lplus l; rewrite H in *; ins; desf; eexists; split; eauto.
  rewrite <- eq_rect_eq in ×.
  by intros; unfold mk_slist in *; desf; ins;
     rewrite in_undup_iff, In_sort, in_app_iff.
Qed.

Lemma res_plus_strip_def r r' :
  res_plus r r' ≠ Rundef →
  res_plus r (res_strip r') ≠ Rundef.
Proof.
  destruct r, r'; ins; desf.
    by rewrite gres_plusC in *; eapply gres_plusA in Heq2;
       eauto using gres_plus_strip_idemp; desf.
  by inv_lplus2 l; ins; unfold prot_plus in *; desf; ins; desf.
Qed.

Lemma res_plus_strip2_def r r' :
  res_plus r r' ≠ Rundef →
  res_plus (res_strip r) (res_strip r') ≠ Rundef.
Proof.
  ins; rewrite <- res_strip_plus; ins; destruct res_plus; ins.
Qed.

Lemma res_plus_escr_def r e :
  r ≠ Rundef →
  res_plus r (Rdef (fun _ ⇒ p_bot) gres_emp e) ≠ Rundef.
Proof.
  by rewrite res_plusC; ins; desf; rewrite ?gres_plusI, ?lift_plus_emp_l in ×.
Qed.

Hint Resolve res_plus_strip_def res_plus_escr_def : rpd.

Lemma res_plus_left_def a b c :
  res_plus a (res_plus b c) ≠ Rundef →
  res_plus a b ≠ Rundef.
Proof.
  by red; intros; rewrite <- res_plusA, H0 in ×.
Qed.

Lemma res_plus_right_def a b c :
  res_plus a (res_plus b c) ≠ Rundef →
  res_plus a c ≠ Rundef.
Proof.
  by red; intros; rewrite res_plusC, res_plusA, H0, res_plusC in ×.
Qed.

Hint Immediate res_plus_left_def res_plus_right_def.

Lemma res_get_upds r l pi : r ≠ Rundef → res_get (res_upd r l pi) l = pi.
Proof.
  destruct r; ins; case eqnP; desf.
Qed.

Lemma res_plus_upd_at r l tau S :
 (res_get r l = p_bot ∨
 ∃ S',
   res_get r l = p_at tau S' ∧
   (∀ s, In s (SL_list S') → In s (SL_list S))) →
 res_upd r l (p_at tau S) =
 res_plus r
     (Rdef (fun x ⇒ if x == l then p_at tau S else p_bot) gres_emp
           (fun _ ⇒ false)).
Proof.
  rewrite res_plusC; ins; desf; try rewrite gres_plusI in *; ins; desf; f_equal;
    try (by extensionality sigma; apply prop_ext; tauto).

  by extensionality l'; inv_lplus l'; desf; ins; desf.
  by exfalso; eapply lift_plus_none_inv in Heq; desf; desf; ins; desf.

  extensionality l'; inv_lplus l'; desf; ins; desf; rewrite <- H1; f_equal.
  apply slist_eq2; ins.
  unfold mk_slist in *; desf; ins; rewrite in_undup_iff, In_sort, in_app_iff.
  rewrite <- eq_rect_eq in ×.
  intuition; eauto.

  exfalso; eapply lift_plus_none_inv in Heq; desf; desf; ins; desf.
  unfold mk_slist in *; desf; ins; destruct n; desf.
  destruct S; ins; split; ins.
    by destruct SL_list; ins.
  rewrite <- eq_rect_eq in ×.
  eapply Sorted_total; eauto; try solve [apply prot_trans_ord];
  rewrite in_app_iff in *; desf; eauto.
Qed.

Lemma res_plus_upd_upd r r' l pi pi' pi'' :
  res_plus r r' ≠ Rundef →
  prot_plus pi pi' = Some pi'' →
  res_plus (res_upd r l pi) (res_upd r' l pi') =
     (res_upd (res_plus r r') l pi'').
Proof.
  destruct r, r'; ins; desf; ins; f_equal.
    by extensionality l'; eapply lift_plus_some_inv with (l:=l') in Heq;
       eapply lift_plus_some_inv with (l:=l') in Heq1; desf; desf.
  eapply lift_plus_none_inv in Heq; desc; inv_lplus l0; desf; desf.
Qed.

Lemma res_get_strip_at r l tau S :
  res_get r l = p_at tau S →
  res_get (res_strip r) l = p_at tau S.
Proof.
  destruct r; ins; rewrite H; ins.
Qed.

Lemma res_get_plus_uninit2 r1 r2 l :
  res_get r1 l = p_uninit →
  res_plus r1 r2 ≠ Rundef →
  res_get r2 l = p_bot.
Proof.
  destruct r1, r2; ins; desf; inv_lplus l; rewrite H in *; ins; desf.
Qed.

Lemma res_get_plus_bot_l r1 r2 l :
  res_get r1 l = p_bot →
  res_plus r1 r2 ≠ Rundef →
  res_get (res_plus r1 r2) l = res_get r2 l.
Proof.
  destruct r1, r2; ins; desf; inv_lplus l; rewrite H in *; ins; desf.
Qed.

Lemma res_get_plus_bot_r r1 r2 l :
  res_get r2 l = p_bot →
  res_plus r1 r2 ≠ Rundef →
  res_get (res_plus r1 r2) l = res_get r1 l.
Proof.
  rewrite res_plusC; apply res_get_plus_bot_l.
Qed.

Lemma res_get_plus_na_l r1 r2 l :
  res_get r1 l = p_uninit ∨ (∃ n, res_get r1 l = p_na pe_full n) →
  res_plus r1 r2 ≠ Rundef →
  res_get (res_plus r1 r2) l = res_get r1 l.
Proof.
  destruct r1, r2; ins; desf; inv_lplus l; rewrite H in *; ins; desf; desf.
Qed.

Lemma res_upd_expand_bot r l pi :
  res_get r l = p_bot →
  res_upd r l pi = res_plus r (res_upd res_emp l pi).
Proof.
  rewrite res_plusC; destruct r; ins; desf;
    try rewrite gres_plusI in *; desf; f_equal.
    extensionality l0; inv_lplus l0; desf; ins; desf.
    destruct pi; ins; desf; congruence.
  exfalso; eapply lift_plus_none_inv in Heq; desf; desf.
  destruct pi; ins; desf.
Qed.

Lemma res_plus_upd_l r r' l pi :
  res_plus r r' ≠ Rundef →
  res_get r' l = p_bot →
  res_plus (res_upd r l pi) r' =
  res_upd (res_plus r r') l pi.
Proof.
  rewrite !(res_plusC _ r'); destruct r, r'; ins; desf; ins; desf.
  f_equal; extensionality l0; inv_lplus l0; desf; desf.
  rewrite H0 in *; ins; desf.
  eapply lift_plus_none_inv in Heq; desc; inv_lplus l0; desf; desf;
  rewrite H0 in *; ins; desf.
Qed.

Lemma prot_plus_get_helper r r' l pi pi' :
  res_get (res_plus r r') l = pi' →
  prot_plus pi' pi = Some pi →
  pi' ≠ p_bot →
  prot_plus (res_get r l) pi = Some pi.
Proof.
  destruct r, r'; ins; desf; ins; desf.
  inv_lplus l.
  destruct (pmap l), (pmap0 l); ins; destruct (p l); ins; destruct pi; ins; desf;
    unfold mk_slist in *; desf; do 2 f_equal.

    by exfalso; eauto using fraction_plusK2.
    by exfalso; eauto using fraction_plusK2.

    eapply slist_eq2; ins.
    assert (In x (SL_list s0) → In x (SL_list s2)).
      rewrite <- H0; simpl; rewrite !in_undup_iff, !In_sort, !in_app_iff.
      rewrite !in_undup_iff, !In_sort, !in_app_iff; tauto.
    rewrite <- H0; ins;
    repeat rewrite !in_undup_iff, !In_sort, !in_app_iff; tauto.

  unfold mk_slist in *; desf; destruct n; split; ins; desf.
    by destruct s as [[]].
  rewrite in_app_iff in ×.
  eapply a1; rewrite in_app_iff, in_undup_iff, In_sort, in_app_iff; tauto.
Qed.

Lemma prot_plus_at_bounded tau S S' :
  (∀ s, In s (SL_list S) → In s (SL_list S')) →
  prot_plus (p_at tau S) (p_at tau S') = Some (p_at tau S').
Proof.
  ins; desf; do 2 f_equal; unfold mk_slist in *; desf.
    eapply slist_eq2; ins; rewrite in_undup_iff, In_sort, in_app_iff;
    rewrite <- eq_rect_eq in *; intuition.
  destruct n; split; ins.
    by destruct S as [[]].
  rewrite in_app_iff in *; destruct S'; ins; rewrite <- eq_rect_eq in *;
  eapply Sorted_total; eauto; try apply prot_trans_ord; desf; eauto.
Qed.

Lemma res_plus_upd_l2 r r' l pi :
  res_plus r r' ≠ Rundef →
  prot_plus (res_get r' l) pi = Some pi →
  res_plus (res_upd r l pi) r' =
  res_upd (res_plus r r') l pi.
Proof.
  rewrite !(res_plusC _ r'); destruct r, r'; ins; desf; ins; desf.
  f_equal; extensionality l0; inv_lplus l0; desf; desf.
  eapply lift_plus_none_inv in Heq; desc; inv_lplus l0; desf; desf.
Qed.

Lemma res_strip_emp : res_strip res_emp = res_emp.
Proof. unfold res_emp; ins; f_equal; apply gres_strip_emp. Qed.

Lemma res_strip_upd r l pi :
  res_strip (res_upd r l pi) = res_upd (res_strip r) l (prot_strip pi).
Proof.
  destruct r; ins; f_equal; extensionality l'; desf; desf.
Qed.

Lemma res_upd_strip_irr r l pi :
  prot_strip (res_get r l) = pi →
  res_upd (res_strip r) l pi = res_strip r.
Proof.
  destruct r; ins; f_equal; extensionality l'; desf; desf; congruence.
Qed.

Lemma res_plus_strip_l r : res_plus (res_strip r) r = r.
Proof. by rewrite res_plusC, res_plus_strip_idemp. Qed.

Lemma res_plus_pcancel :
  ∀ r a b,
    res_plus r a = res_plus r b →
    res_plus r a ≠ Rundef →
    res_plus (res_strip r) a = res_plus (res_strip r) b.
Proof.
  destruct r; ins; desf; f_equal; ins;
    try (pose proof (gres_pcancel Heq6 Heq4); congruence);
    first [extensionality l | exfalso ];
    inv_lplus2 l; destruct (pmap l); ins; desf; try congruence.
  by exfalso; rewrite <- H4 in *; desf; eauto using fraction_plusK1, fraction_plusK2.
  by exfalso; rewrite <- H4 in *; desf; eauto using fraction_plusK1, fraction_plusK2.
  rewrite <- H4 in *; desf; pose proof (fraction_plusK _ _ _ Heq7 Heq8); congruence.
Qed.

Definition rknow r := r = res_strip r.

Lemma res_plus_ubound r r' :
    r ≠ Rundef →
    r = res_plus r r' →
    rknow r'.
Proof.
  unfold rknow; rewrite <- (res_plus_emp_r r) at 2; intros.
  apply res_plus_pcancel in H0;
    rewrite res_plus_emp_r in *; ins.
  destruct r, r'; ins; desf; clear H0; desf; f_equal;
    eauto using eq_sym, gres_strip_max.
  extensionality l; inv_lplus l.
  by destruct (pmap l); ins; desf; rewrite H1 in ×.
Qed.

Lemma gknow_plusE g g' gg :
  gres_plus g g' = Some gg →
  gg = gres_strip gg →
  g = gres_strip g ∧ g' = gres_strip g'.
Proof.
  ins; assert (A := gres_plus_strip_idemp gg).
  eapply (gres_plusA H) in A; desf; rewrite <- H0 in ×.
  split; symmetry; rewrite gres_plusC in *; eauto using gres_strip_max.
Qed.

Lemma rknow_plusE r r' :
  res_plus r r' ≠ Rundef →
  (rknow (res_plus r r') ↔ rknow r ∧ rknow r').
Proof.
  split; ins; desf; unfold rknow in *; rewrite ?res_strip_plus; try congruence.
  destruct r, r'; ins; desf; ins; desf.
  destruct (gknow_plusE _ _ Heq0 H0); split; f_equal; desf;
  extensionality l; inv_lplus l; rewrite H2 in Heq; clear H2;
  destruct (pmap l), (pmap0 l); ins; destruct (p l); ins; desf; desf.
Qed.

Lemma res_plus_eq_empD r r' : res_plus r r' = res_emp → r = res_emp ∧ r' = res_emp.
Proof.
  unfold res_emp; destruct r; ins; desf; split; ins; f_equal; ins;
  eauto using gres_eq_empD; rewrite gres_plusC in *; eauto using gres_eq_empD;
  extensionality x; try inv_lplus x;
    try apply (f_equal (fun f ⇒ f x)) in H; unfold prot_plus in *; desf; desf.
Qed.

Lemma rsum_eq_empD l : rsum l = res_emp → ∀ r, In r l → r = res_emp.
Proof.
  induction l; ins; apply res_plus_eq_empD in H; desf; eauto.
Qed.

Lemma res_plus_get1 r r' l :
  res_plus r r' ≠ Rundef →
  prot_plus (res_get r l) (res_get r' l) ≠ None.
Proof.
  destruct r, r'; ins; desf.
  eapply lift_plus_some_inv with (l:=l) in Heq; congruence.
Qed.

Lemma res_plus_get2 r r' l :
  prot_plus (res_get r l) (res_get r' l) = None →
  res_plus r r' = Rundef.
Proof.
  destruct r, r'; ins; desf.
  eapply lift_plus_some_inv with (l:=l) in Heq; congruence.
Qed.

Lemma res_escr_upd r l pi sigma :
  res_escr (res_upd r l pi) sigma ↔ res_escr r sigma.
Proof. destruct r; ins. Qed.

Lemma res_escr_mupd r l n pi sigma :
  res_escr (res_mupd r l n pi) sigma ↔ res_escr r sigma.
Proof. destruct r; ins. Qed.

Lemma res_escr_plusE r r' sigma :
  res_escr (res_plus r r') sigma → res_escr r sigma ∨ res_escr r' sigma.
Proof.
  unfold res_plus; desf; ins; destruct (escr sigma); vauto.
Qed.

Lemma res_escr_plusI r r' sigma :
  res_plus r r' ≠ Rundef →
  res_escr r sigma ∨ res_escr r' sigma → res_escr (res_plus r r') sigma.
Proof.
  unfold res_plus; desf; ins; desf; apply orbT.
Qed.

Lemma res_escr_plus r r' (D: res_plus r r' ≠ Rundef) sigma :
  res_escr (res_plus r r') sigma ↔ res_escr r sigma ∨ res_escr r' sigma.
Proof.
  split; eauto using res_escr_plusI, res_escr_plusE.
Qed.

Lemma res_escr_strip :
  ∀ r sigma, res_escr (res_strip r) sigma ↔ res_escr r sigma.
Proof.
  by destruct r.
Qed.

Lemma res_get_sum:
  ∀ r loc tau (S : slist tau) l,
  res_get r loc = p_at tau S →
  rsum l ≠ Rundef →
  In r l →
  ∃ S' : slist tau,
    res_get (rsum l) loc = p_at tau S' ∧
    (∀ s : prot_state tau, In s (SL_list S) → In s (SL_list S')).
Proof.
  induction l; ins; desf.
    by eapply res_get_plus.
  edestruct IHl; desc; eauto.
    by destruct a; ins; desf.
  rewrite res_plusC in *;
    exploit res_get_plus; eauto.
  intro; desf; eauto.
Qed.

Lemma res_get_of_strip_eq r r' l tau S :
  res_strip r = res_strip r' →
  res_get r' l = p_at tau S →
  res_get r l = p_at tau S.
Proof.
  destruct r, r'; ins; desf.
  apply f_equal with (f:=fun x ⇒ x l) in H3.
  destruct (pmap l), (pmap0 l); ins; desf.
Qed.

Lemma res_plus_eq_empI r r' :
  r = res_emp → r' = res_emp → res_plus r r' = res_emp.
Proof.
  intros; desf; apply res_plus_emp_r.
Qed.

Lemma rsum_map_map_eq_empI A B f (g: A → B) l :
  (∀ x, In x l → f (g x) = res_emp) →
  rsum (map f (map g l)) = res_emp.
Proof.
  induction l; ins; rewrite H, res_plus_emp_l; eauto.
Qed.

Lemma res_gget_def r mm gone :
  res_gget r mm = None →
  r ≠ Rundef →
  res_plus r (Rdef (fun _ ⇒ p_bot) (gres_one mm gone) (fun _ ⇒ false)) ≠ Rundef.
Proof.
  destruct r; ins; desf; unfold gres_plus in *; try done.
  2: by rewrite lift_plus_noneD in *; unfold prot_plus in *; desf.
  des_eqrefl; ins; symmetry in EQ; rewrite lift_plus_noneD in EQ; desf; desf.
    by rewrite H in EQ.
  by destruct (gres x).
Qed.

Lemma res_gget_def2 r p g e mm gone :
  r = Rdef p g e →
  res_gget r mm = None →
  ∃ g', gres_plus g (gres_one mm gone) = Some g' ∧
  res_plus r (Rdef (fun _ ⇒ p_bot) (gres_one mm gone) (fun _ ⇒ false)) = Rdef p g' e.
Proof.
  ins; desf; ins.
  cut (∃ g', gres_plus g (gres_one mm gone) = Some g').
    rewrite lift_plusC, lift_plus_emp_l; ins; desf; eauto using prot_plusC.
    by eexists; split; ins; f_equal; extensionality y; apply orbF.
  unfold gres_plus; des_eqrefl; vauto.
  exfalso; symmetry in EQ; rewrite lift_plus_noneD in EQ; desf; ins; desf; desf.
    by rewrite H0 in EQ.
  by destruct (g x).
Qed.

Lemma res_gget_plus r1 r2 mm :
  res_gget (res_plus r1 r2) mm = None ↔
  res_plus r1 r2 = Rundef ∨
  res_gget r1 mm = None ∧
  res_gget r2 mm = None.
Proof.
  destruct r1, r2; ins; desf; split; ins; try tauto; desf;
    unfold gres_plus in *; des_eqrefl; desf; ins; [right|];
    inv_lplus mm; rewrite H in *; ins; desf.
    by destruct (gres mm), (gres0 mm); ins; desf.
  ins; congruence.
Qed.

Lemma res_gget_rsum rl mm :
  res_gget (rsum rl) mm = None ↔
  rsum rl = Rundef ∨ ∀ r, In r rl → res_gget r mm = None.
Proof.
  induction rl; ins; try tauto.
  rewrite res_gget_plus, IHrl; clear; split; ins; desf; eauto 8.
    by rewrite H0, res_plus_undef; vauto.
  by right; ins; desf; eauto.
Qed.

Lemma res_lt_strengthen r r' :
  (r' ≠ Rundef → res_lt r r') → res_lt r r'.
Proof.
  destruct r'; ins; [by ∃ Rundef; destruct r|by apply H].
Qed.

Lemma res_lt_strip_frame r r' f :
  res_lt (res_strip r) (res_strip r') →
  res_plus r f ≠ Rundef →
  res_lt (res_strip (res_plus r f)) (res_strip (res_plus r' f)).
Proof.
  ins; apply res_lt_strengthen; intro B.
  destruct H as [m H]; rewrite !res_strip_plus; ins.
    by ∃ m; rewrite <- H, !(res_plusC _ m), res_plusA.
  by intro X; rewrite X in ×.
Qed.

Lemma res_lt_frame_l r r' f : res_lt r r' → res_lt (res_plus f r) (res_plus f r').
Proof.
  unfold res_lt; ins; desf; eauto using res_plusA.
Qed.

Lemma res_lt_frame_r r r' f : res_lt r r' → res_lt (res_plus r f) (res_plus r' f).
Proof.
  rewrite !(res_plusC _ f); apply res_lt_frame_l.
Qed.

Lemma res_lt_plus_l r r' f : res_lt r r' → res_lt r (res_plus f r').
Proof.
  unfold res_lt; ins; desf; eauto using res_plusAC.
Qed.

Lemma res_lt_plus_r r r' f : res_lt r r' → res_lt r (res_plus r' f).
Proof.
  rewrite res_plusC; apply res_lt_plus_l.
Qed.

Lemma res_lt_plus :
  ∀ r r' (L: res_lt r r') s s' (L' : res_lt s s'),
    res_lt (res_plus r s) (res_plus r' s').
Proof.
  unfold res_lt; ins; desf.
  rewrite !res_plusA, (res_plusAC s), <- res_plusA; eauto.
Qed.

Lemma res_lt_strip_l r r' :
  res_lt (res_strip r) r' ↔ res_lt (res_strip r) (res_strip r').
Proof.
 unfold res_lt; split; ins; desf.
   case_eq (res_plus (res_strip r) r_rem) as X.
     by ∃ Rundef; case r.
   by rewrite <- X, res_strip_plus, res_strip_idemp; vauto; rewrite X.
 by ∃ (res_plus r_rem r'); rewrite <- res_plusA, H, res_plusC, res_plus_strip_idemp.
Qed.

Lemma res_lt_frame_rev r a b:
  res_lt (res_plus r a) (res_plus r b) →
  res_lt (res_strip r) b →
  res_plus r b ≠ Rundef →
  res_lt a b.
Proof.
  unfold res_lt in *; ins; desf.
  rewrite <- res_plusA, res_plus_strip_idemp, res_plusA in ×.
  eapply res_plus_pcancel in H; try congruence.
  rewrite res_plusAC in H; vauto.
Qed.

Lemma res_add_strip_stengthen r r' :
  (∃ rem, r = res_plus r' rem) →
  (∃ rem, r = res_plus r' rem ∧ res_lt (res_strip r') rem).
Proof.
  ins; desf; ∃ (res_plus (res_strip r') rem); split; vauto.
  by rewrite <- res_plusA, res_plus_strip_idemp.
Qed.