proposition: Lemma f_star_eq_sos : forall r i r' i', (exists n, f_star n r i = Some(r',i'))<->sos_star r i i' r'.
proof: Proof. intros r i r' i'; split; [intros [n Hn]; apply f_star_sem with n; auto| apply sos_star_f; auto]. Qed.
imports: ZArith List syntax Lia