proposition: Lemma Exercise4_6g h: E46_hp h -> exists k, [/\ natp k, k <=c h & Exercise4_5_conc E46_order_r (n +c k)].
proof: Proof. move=> [hN _ hprop _]; move: (Exercise4_6f hN hprop). move=> [k [kN pa pb]]; exists k; split => //. move: Exercise4_6a => [[oR sR] rR]. exact: (Exercise4_5d oR (NS_sum nN kN) pb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)