proposition: Lemma coarserA x: {when partition_s ^~ x &, antisymmetric_r coarser_cs}.
proof: Proof. suff: (forall y y', partition_s y x -> partition_s y' x -> coarser_cs y y' -> coarser_cs y' y -> sub y y'). move=> hyp u v p1 p2 c1 c2. apply: extensionality; first exact: (hyp _ _ p1 p2 c1 c2). by apply: (hyp _ _ p2 p1 c2 c1). move=> y y' [p1 ne] _ c1 c2 t ty. move: (c2 _ ty)(ne _ ty) => [b by' tb] [z zt]. move:(c1 _ by') => [a ay ba]. case: ((proj2 p1) _ _ ty ay) => eq; last by empty_tac1 z. have -> //: t = b by apply: extensionality=>//; rewrite eq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)