proposition: Lemma Lt_Gt : forall x y, string_compare x y = Gt <-> string_compare y x = Lt.
proof: Proof. intros x; induction x as [ | x0 x' Hind ]; intros y; destruct y as [ | y0 y' ]; simpl; split; first [ discriminate | trivial ]; destruct (nat_compare_consistent (nat_of_ascii x0) (nat_of_ascii y0)) as [ [ (H1, H2) | (H1, H2) ] | (H1, H2) ]; rewrite H1, H2; try rewrite Hind; auto. Qed.
imports: Coq.ZArith.ZArith Coq.Strings.String Coq.Strings.Ascii Coq.Structures.OrderedType Fiat.Common.Coq__8_4__8_5__Compat