lemmas i01 and fix

Author: mkerjean

theories/hahn_banach_theorem.v

@@ -202,14 +202,23 @@ Hypothesis p_cvx : (@convex_function  R V [set: V]  p).
   real line directed by an arbitrary vector v *)
 
  Lemma divDl_ge0 (s t : R) (s0 : 0 <= s) (t0 : 0 <= t) : 0 <= s / (s +t).
- Admitted.
-
+ by apply: divr_ge0 => //; apply: addr_ge0.
+ Qed.
+ 
  Lemma divDl_le1 (s t : R) (s0 : 0 <= s) (t0 : 0 <= t) :  s / (s +t) <= 1.
- Admitted.
-
- Lemma divD_onem (s t : R) : (s / (s + t)).~ = t / (s + t).
- Admitted. 
-
+ move: s0; rewrite le0r => /orP []; first by move => /eqP ->; rewrite mul0r //.
+ move: t0; rewrite le0r => /orP [].
+   by move => /eqP -> s0; rewrite addr0 divff //=; apply: lt0r_neq0. 
+ by move=> t0 s0; rewrite ler_pdivrMr ?mul1r ?addr_gt0 // lerDl ltW.
+ Qed.    
+
+ Lemma divD_onem (s t : R) (s0 : 0 < s) (t0 : 0 < t): (s / (s + t)).~ = t / (s + t).
+ rewrite /(_).~.
+ suff -> : 1 = (s + t)/(s + t) by rewrite -mulrBl -addrAC subrr add0r. 
+ rewrite divff // /eqP addr_eq0; apply/negbT/eqP => H.
+ by move: s0; rewrite H oppr_gt0 ltNge; move/negP; apply; rewrite ltW.
+ Qed.
+ 
  Lemma domain_extend  (z : zorn_type) v :
      exists2 ze : zorn_type, (zorn_rel z ze) & (exists r, (carrier ze)  v r).
  Proof.
@@ -386,7 +395,7 @@ have graphFP : spec F f p graphF by split.
 have [z zmax]:= zorn_rel_ex graphFP.
 pose FP v : Prop := F v.
 have FP0 : FP 0 by [].
-have [g gP]:= (hb_witness linfF FP0 p_cvx sup inf graphFP zmax).
+have [g gP]:= (hb_witness linfF FP0 p_cvx sup inf zmax).
 have scalg : linear_for *%R g.
   case: z {zmax} gP=> [c [_ ls1 _ _]] /= gP.
   have addg : additive g.