proposition: Lemma maxS (x y: R) (z := (Num.max x y) +1) : (x<z) && (y <z).
proof: Proof. have p1 : forall u v:R, u <= v -> u < v + 1. by move=> u v h; rewrite (le_lt_trans h) // ltr_addl ltr01. by rewrite !p1// ?le_maxr// lexx // orbT. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)