proposition: Lemma ord_cofinal_p1 A B: ordinal_set B -> (ord_cofinal A B <-> cofinal (ole_on B) A).
proof: Proof. move => h. have pa: (substrate (ole_on B)) = B. rewrite graph_on_sr // => c /h oc; fprops. split. move => [sa sb]; hnf; rewrite pa; split => //. move => x xb; move: (sb _ xb) => [y ya xy]; exists y => //. by apply /graph_on_P1; split => //; apply: sa. rewrite /cofinal pa; move => [sa sb]; split => // x xb. move:(sb _ xb) => [y ya /graph_on_P1 [_ yb yx]]; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)