proposition: Lemma StronglySorted_app_r A r (l l': list A): StronglySorted r (l ++ l') -> StronglySorted r l'.
proof: Proof. rewrite StronglySorted_app_iff; tauto. Qed.
imports: HahnBase HahnSets HahnList HahnRelationsBasic HahnEquational Sorted Setoid