proposition: Lemma Ex6_32p4c3 A B k0: Exercise6_32_hyp A B k0 -> natp k0 -> supp_left_unbounded (fdfc A) -> supp_left_unbounded (fdfc B).
proof: Proof. move => /Ex6_32_HS ha hb hc; ex_middle hd. by case:(Ex6_32p4c1 ha hb hd). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)