proposition: Lemma T1toB_surjective x: x <o epsilon0 -> exists y, x = T1toB y.
proof: Proof. move => xo; move:(proj31_1 xo) => ox; move: xo. case:(least_ordinal6 (fun z => z <o epsilon0 -> exists y, z = T1toB y) ox) =>//. set z := least_ordinal _ _. move => [oz Hz []] zo. case: (ozero_dichot oz); first by move => ->; exists zero. move => h; move: (CNF_simple_bdn2 h zo). move:(the_CNF_simplP h). set a := (P (the_CNF_simpl z)). set b:= (P (Q (the_CNF_simpl z))). set c:=(Q (Q (the_CNF_simpl z))). move => ax [ha hb]. have ae:= olt_ltT ha zo. have ce:=olt_ltT hb zo. move/(oltP oz): ha => az. move/(oltP oz): hb => cz. move: (Hz _ az ae) => [a' a'v]. move: (Hz _ cz ce) => [c' c'v]. move: ax => [qa qb qc qd qe]. move: (nat_to_B_surjective qc) => [n' n'v]. by exists (cons a' n' c'); simpl; rewrite - n'v - a'v - c'v. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)