proposition: Theorem restr_plus_interval_is a b (f := (rest_plus_interval a b)) (g := (rest_minus_interval a b)): natp a -> natp b -> [/\ bijection f, bijection g, g = inverse_fun f & order_isomorphism f (Nint_cco \0c a) (Nint_cco b (a +c b))].
proof: Proof. move=> aN bN. have zN:= NS0. have abN:= (NS_sum aN bN). set E1:= Nintc a. set E2:= Nintcc b (a +c b). have tap: lf_axiom (fun z => z +c b) E1 E2. move => z /(NintcP aN) za; apply/(Nint_ccP1 bN abN); split. by apply: Nsum_Mle0. by apply: csum_Mleeq. have tam: lf_axiom (fun z => z -c b) E2 E1. move => z /(Nint_ccP1 bN abN) [bt tab]; apply /(NintcP aN). move: (NS_diff b (NS_le_nat tab abN)) => sN; apply: cdiff_Mle =>//. have ff:function f by apply: lf_function. have fg:function g by apply: lf_function. have sf:source f = target g by rewrite lf_source lf_target. have sg:source g = target f by rewrite lf_source lf_target. have cfg:f \coP g by []. have cgf: g \coP f by []. have c1: g \co f = identity (source f). apply: function_exten; [fct_tac | fprops | by aw | by aw | ]. rewrite compf_s;move=> x xsf /=. rewrite (idV xsf) compfV //. move: xsf; rewrite lf_source=> xs. rewrite (LfV tap xs) (LfV tam (tap _ xs)). rewrite cdiff_pr1 =>//; apply: (Nint_S xs). have c2: f \co g = identity (source g). apply: function_exten ; [fct_tac | fprops | by aw | by aw | ]. rewrite compf_s;move=> x xsg /=. rewrite (idV xsg) (compfV cfg xsg). move: xsg; rewrite lf_source=> xs. rewrite (LfV tam xs). have xN:=(Nint_S xs). move: xs => /(Nint_ccP1 bN abN) [bx xaN]. have aux: inc (x -c b) (Nintcc \0c a). apply/(NintcP aN); apply: cdiff_Mle =>//. rewrite (LfV tap aux) csumC cdiff_pr //. move: (bijective_from_compose cgf cfg c1 c2)=> [bf bg gif]; split => //. have sp : E1 = source (rest_plus_interval a b). by rewrite /rest_plus_interval; aw. move: (Ninto_wor \0c a) => [[o1 _ ] sr1]. move: (Ninto_wor b (a +c b))=> [[o2 _ ] sr2]. hnf;rewrite /bijection_prop sr1 sr2 lf_source lf_target;split => //. move=> x y /=; rewrite lf_source => xsf ysf. rewrite (LfV tap xsf) (LfV tap ysf). split; move /Ninto_gleP => [pa pb pc]; apply/Ninto_gleP. by split; try (apply: tap => //); apply: csum_Mleeq. split=> //; apply:(csum_le2l bN (Nint_S xsf) (Nint_S ysf)). by rewrite csumC (csumC b y). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)