proposition: Lemma dhomog_msize d p : p \is d.-homog -> p \is (mfsize p).-1.-homog.
proof: Proof. rewrite mmeasureE => /dhomogP h; apply/dhomogP => m m_in_p. rewrite h // big_seq (eq_bigr (fun _ => d.+1)); last by move=> i /h ->. rewrite -big_seq (perm_big _ (perm_to_rem m_in_p)) big_cons /=. elim: (rem _ _)=> [|x s ih]; first by rewrite big_nil maxn0. by rewrite big_cons maxnA maxnn -ih. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg