proposition: Lemma P_well_founded_induction_type : well_founded_P -> forall Q : A -> Type, (forall x : A, P x -> (forall y : A,P y-> R y x -> Q y) -> Q x) -> forall a : A, P a -> Q a.
proof: Proof. move => W Q Ha a. have wfr: well_founded restrict by move => b; split => y [ra _ _]; apply: W. apply: (well_founded_induction_type wfr (fun x => P x -> Q x)). by move => x Hb px; apply: Ha => // y py ry; apply: Hb. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)