proposition: Lemma Exercise1_21r r: total_order r -> exists r' g', [/\ orsum_ax r' g', orsum_ax2 g', r \Is (order_sum r' g'), (small_set (substrate r') \/ without_gaps r') & allf g' scattered].
proof: Proof. set (s:= (scattered_equiv r)) => tor. move: (@Exercise1_2i r s) => /=. have p1: weak_order_compatibility r s by apply: Exercise1_21m. have p2: Ex1_2_hC' r s by apply: Exercise1_21o. move=> h; move: (h p1 p2 tor). set q:= quotient s; set d := (disjointU _). move => [q1 q2 q3 q4 [q5 q6]] {h}. exists (quotient_order r s); exists(Lg q(fun z => induced_order r z)). split => //. - by exists (Lf (fun x => J x (class s x)) (substrate r) d). - by apply: Exercise1_21q. - rewrite/allf;aw;move=> i idg; rewrite LgV//; move: idg => /funI_P [z zs] ->. by apply: (Exercise1_21n tor); rewrite - (Exercise1_21j tor). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)