proposition: Lemma decides_dec_lt : forall n n', decides (if (Compare_dec.lt_dec n n') then true else false) (lt n n').
proof: Proof. intros; find_if_inside; simpl; eauto. Qed.
imports: Fiat.Computation Fiat.Common.DecideableEnsembles Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.Notations