proposition: Lemma odiff_wrong_alt a b (c := ordinal (induced_order (ordinal_o b) (b -s a))): b <=o a -> c = \0c.
proof: Proof. rewrite /c; move=> [oa ob ab];rewrite (setC_T ab). have oon: order (ordinal_o b) by apply: ordinal_o_or. apply: ordinal0_pr1; rewrite iorder_sr; fprops. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)