proposition: Lemma ord_induction_p01 x: OIax1 -> u <=o x -> f x \0o <o f x \1o.
proof: Proof. by move => [h _ _] ux; rewrite fv ord_induction_y0 ord_induction_y1; apply:h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)