proposition: Lemma f91 n : (f91_exists n).1 = if le_lt_dec n 100 then 91 else n - 10.
proof: Proof. destruct f91_exists. simpl. generalize (f91_spec _ _ pr2). destruct le_lt_dec; auto. Qed.
imports: Equations(Equations) Arith Lia Relations Utf8