proposition: Lemma build_trs_proof : forall i, exists j, i <= j /\ E! (f j) (g j).
proof: Proof. intro i. apply not_all_not_ex. intro HTF. induction i. assert (HT : IS R g). intro k. gen (hyp1 (S k)). gen (HTF (S k)). rewrite not_and_eq. intro HT. destruct HT as [HT | HT]. destruct (HT (Nat.le_0_l (S k))). intro HT0. destruct (rtc_split (proj1 HT0)) as [HT1 | HT1]. rewrite <- HT1. apply (proj2 (hyp1 k)). tauto. apply (@NISR g). hyp. assert (HT : forall j, ~ ((E !) (f (S i + j)) (g (S i + j)))). intro j. gen (HTF (S i + j)). apply contraposee_inv. intro HT. split; try lia. hyp. assert (HT0 : forall j, (f (S i + j)) = (g (S i + j))). intro j. destruct (rtc_split (proj1 (hyp1 (S i + j)))); auto. destruct (HT j); auto. pose (h := fun j => g (S i + j)). assert (IS R h). intro j. unfold h. rewrite <- (HT0 (S j)). gen (proj2 (hyp1 (S i + j))). rewrite <-Nat.add_succ_r. simpl. auto. gen H. apply NISR. Qed.
imports: CoLoR(RelUtil NatUtil Path LeastNat LogicUtil ClassicUtil SN NotSN_IS SortUtil ListUtil) Coq(IndefiniteDescription)