proposition: Lemma le_witness_informative : forall m n : nat, m <= n -> {k : nat | n = m + k}.
proof: Proof. intros. induction n as [| n Hrecn]. exists 0. rewrite <- (plus_n_O m). symmetry in |- *. apply Nat.le_0_r. assumption. case (le_lt_eq_dec m (S n)). assumption. intro. case Hrecn. apply Nat.lt_succ_r. assumption. intro k. intros. exists (S k). rewrite <- (Nat.add_succ_comm m k). simpl in |- *. apply eq_S. assumption. intro. exists 0. rewrite <- (plus_n_O m). symmetry in |- *. assumption. Qed.
imports: CoRN.reals.Bridges_LUB