proposition: Lemma nat_cofe' : forall A {IA:Inhab A} (sim:nat->binary A), (forall i, equiv (sim i)) -> nat_complete' sim -> COFE (nat_family sim).
proof: Proof. Proof using. introv IA Equiv Comp. asserts Ofe: (OFE (nat_family sim)). constructor; simpl. apply wf_lt. intros_all~. math. apply Equiv. constructor~. apply~ complete_of_locally_and_globally_complete. introv Cohu. sets v: (fun j => If j < i then u j else u (i-1)%nat). forwards [l L]: (Comp v). intros k j Rkj. tests: (S j < i). unfold v. do 2 case_if; try math. apply Cohu; hnf; math. unfold v. tests: (j < i). math_rewrite ((i - 1)%nat = j). case_if; try math. apply Cohu; hnf; math. case_if. tests: (k = (i -1)%nat). apply~ equiv_refl. apply Cohu; hnf; try math. apply~ equiv_refl. exists l. intros j Rji. unfolds inverse. simpls. specializes L j. unfold v in L. case_if~; try false. introv Cohu. forwards [l L]: (Comp u). intros i. induction_wf IH: lt_wf i. intros. apply~ Cohu. exists l. introv _. apply L. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)