proposition: Lemma proj_satP : DecidableField.axiom proj_sat.
proof: Proof. move=> e f; have fP := quantifier_elim_rformP e (to_rform_rformula f). by apply: (iffP fP); move/to_rformP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)