proposition: Lemma SymTrans_CompatR {A} (cmp:A->A->comparison) : SymTrans cmp -> CompatR cmp.
proof: Proof. intros (Sy,Tr) x y y' Hy. destruct (cmp x y) eqn:E, (cmp x y') eqn:E'; trivial. - erewrite Tr in E'; eauto. - erewrite Tr in E'; eauto. - erewrite Tr in E; eauto. now flipcmp Hy. - flipcmp E. erewrite Tr in Hy; eauto. easy. - flipcmp Hy. erewrite Tr in E; eauto. - flipcmp E. erewrite Tr in Hy; eauto. easy. Qed.
imports: Coq(List)