proposition: Lemma split_string_ValidDomainName_length : forall d, d <> ""%string -> lt (String.length (snd (split_string d))) (String.length d).
proof: Proof. induction d; simpl; intros; try congruence. destruct (Ascii.ascii_dec a "."); simpl; eauto. destruct d; simpl in *; eauto. destruct (if Ascii.ascii_dec a0 "." then (""%string, d) else (let (s1, s2) := split_string d in (String a0 s1, s2))). simpl in *. etransitivity. apply IHd. congruence. eauto with arith. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Arith.PeanoNat Coq.Strings.Ascii Coq.Strings.String Fiat.Common.List.Operations Fiat.Common.StringOperations