proposition: Lemma BR_seq_prop1 f: (forall n, natp n -> realp (f n)) -> BR_seq (Lg Nat f).
proof: Proof. move => h. have sa:fgraph (Lg Nat f) by fprops. have sb: (domain (Lg Nat f)) = Nat by aw. by split => // t /(range_gP sa); rewrite sb; move => [n na ->]; rewrite LgV//; apply: h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)