proposition: Lemma Exercise4_6b h: h <=c m -> E46_hprop h -> m <=c (n +c h).
proof: Proof. move => hm hp; move: (NS_le_nat hm mN) => hN. move: (NS_diff h mN)(cdiff_pr hm); set r := (m -c h); move=> rN phm. have pa: r <=c (m -c h) by rewrite -/r; fprops. have pb: sub (domain X) (domain X) by fprops. have pc: cardinal (domain X) = r +c h. by rewrite csumC phm; move: Xpr => [_ ok _ _]. move: (hp _ _ pa pb pc) => [T [Td cT _]]. move: (sub_smaller Td); move: Ypr => [_ cdY _ _]; rewrite cT cdY. have lehh: h <=c h by fprops. by move=> pd; move: (csum_Mlele pd lehh); rewrite csumC phm. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)