proposition: Lemma T1transfinite_induction_Q (P: T1 -> Type) (Q: T1 -> Prop): (forall x:T1, Q x -> T1nf x -> (forall y:T1, Q y -> T1nf y -> y < x -> P y) -> P x) -> forall a, T1nf a -> Q a -> P a.
proof: Proof. pose q a:= T1nf a /\ Q a; pose lt x y := x < y. move => H a pa pb; move: {pa pb} a (conj pa pb). have wf1: well_founded_P q lt. move => a qa; elim: (nf_Wf' (proj1 qa)). by move => b _ h2; split => c [ [na _] la [nb _]]; apply: h2. have H': forall x, q x -> (forall y, q y -> lt y x -> P y) -> P x. by move => x [pa pb] ha; apply: H => // y ya yb; apply: ha. exact: (P_well_founded_induction_type wf1 H'). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)