proposition: Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
proof: Proof. intros x y z; generalize x z; clear x z; induction y; destruct x; destruct z; intros; unfold lt in *; simpl in *; first [ discriminate | destruct_comparisons; comparisons_minicrush | trivial ]; intuition. Qed.
imports: Coq.ZArith.ZArith Coq.Strings.String Coq.Strings.Ascii Coq.Structures.OrderedType Fiat.Common.Coq__8_4__8_5__Compat