proposition: Lemma Ex6_32p4c2 A B k0: Exercise6_32_hyp A B k0 -> natp k0 -> ~ supp_right_unbounded (fdfc A) -> ~ supp_right_unbounded (fdfc B).
proof: Proof. move => Hab kn hh. case:(all_exists_dichot2 (fun a => forall x, a <=z x -> Vg (fdfc A) x = \0c) BZ). move => H; case: hh => i iz. case:(all_exists_dichot2 (fun j => i <=z j /\ Vg (fdfc A) j <> \0c) BZ). move => HH; case: (H _ iz) => x xx; ex_middle bad. by case:(HH _ (proj32 xx)). by move => [j _ [HA HB]]; exists j. move =>[a az etc]. move: (Ex6_32p4b Hab kn az etc) => Ha bad. by move: (bad _ (ZSs az (ZNz kn))) => [j lja]; case; apply: Ha. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)