proposition: Lemma props_of_b: [/\ ordinalp gamma, gamma <> \0o & \0o <o gamma].
proof: Proof. move: bg2 => [_ ob _]. have bp:= (olt_leT (olt_02) bg2). move: (bp) => [_ /nesym bne] //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)