proposition: Lemma fusc_pr: fusc_prop fusc.
proof: Proof. move:Nat_order_wor => [pa pb]. move:(transfinite_defined_pr (fun u => (fusc_next u (source u))) pa). set F := transfinite_defined _ _;move => [[ff _] hb hc]. rewrite pb in hc hb. have hi: forall x, natp x -> source (restriction1 F (segment Nat_order x)) = x. move => x xN; rewrite / restriction1; aw. by rewrite (segment_Nat_order1 xN). have hc1: forall x, inc x Nat -> Vf F x = fusc_next (restriction1 F (segment Nat_order x)) x. by move => x xn; move:(hc _ xn); rewrite (hi _ xn). have hd: forall n, fusc n = Vf F n by done. have he: fusc \0c = \0c by rewrite hd (hc1 _ NS0) /fusc_next; Ytac0. have hf: fusc \1c = \1c. by rewrite hd (hc1 _ NS1) /fusc_next(Y_false card1_nz); Ytac0. have hg: forall n, natp n -> sub (segment Nat_order n) (source F). by move => n nN; rewrite hb => t /Zo_S; rewrite pb. have hh: forall n m, n <c m -> natp m -> inc n (segment Nat_order m). move => n m lnm mN; rewrite (segment_Nat_order1 mN). apply/oltP;[ by move/NatP:mN => [] | by apply: oclt]. have hj:forall n, natp n -> fusc (\2c *c n) = fusc n. move => n nN; move:(NS_double nN) => n2N. case: (equal_or_not n \0c) => nz; first by rewrite nz cprod0r. have [qa qc]:=(double_nz nN nz). have qb:= (even_double nN). have qe:= even_half nN. rewrite !hd (hc1 _ n2N) /fusc_next qe; Ytac0; Ytac0; Ytac0. have qf := (hh _ _ (clt_n_doublen nN nz) n2N). by rewrite (restriction1_V ff (hg _ n2N) qf). split => //. move => n nN; move:(NS_double nN) => n2N; move:(NS_succ n2N) => n3N. case: (equal_or_not n \0c) => nz. by rewrite nz cdouble0 succ_zero he hf (csum0l CS1). have [qa qb]:=(doubleS_nz nN nz). have qc:= (proj2 (succ_of_even (even_double nN))). have qg: csucc n <c (csucc (\2c *c n)) by apply cltSS; apply: clt_n_doublen. rewrite !hd (hc1 _ n3N) /fusc_next (odd_half nN); Ytac0; Ytac0; Ytac0. rewrite (restriction1_V ff (hg _ n3N) (hh _ _ qg n3N)). by rewrite (restriction1_V ff (hg _ n3N) (hh _ _ (cle_ltT (cleS nN) qg) n3N)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)