proposition: Lemma fib_OK0 : forall n, fib_iter n (1,1) = (fib (S n), fib n).
proof: Proof. induction n; simpl; auto. destruct n. - cbn; reflexivity. - rewrite IHn; unfold fib_step. simpl fst; simpl snd; auto. Qed.
imports: hydras(primRec cPair extEqualNat)