proposition: Lemma head_unif_part x0 (a b : R) (n : nat) : head x0 (unif_part a b n) = a.
proof: Proof. rewrite /= Rmult_0_l /Rdiv ; ring. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy