proposition: Lemma cmp_lt_trans : forall x y z, cmp x y = Lt -> cmp y z = Lt -> cmp x z = Lt.
proof: Proof. induction x; destruct y; destruct z; simpl; try (refl||discr). apply BCmpTransLeibniz.cmp_lt_trans. case_eq (cmp x1 y1); intro e1; try (refl||discr). apply cmp_eq in e1. subst. case_eq (cmp y1 z1); intro e2; try (refl||discr). apply cmp_eq in e2. subst. fo. intros _. case_eq (cmp y1 z1); intro e2; try (refl||discr). apply cmp_eq in e2. subst. case_eq (cmp y2 z2); intro e2; try (refl||discr). intros _. case_eq (cmp x1 z1); intro e3; try (refl||discr). apply cmp_eq in e3. subst. Module CF := CmpFacts C. rewrite CF.eq_refl in e1. discr. rewrite e1 in e3. auto. intros _. case_eq (cmp x1 z1); intro e3; try (refl||discr). apply cmp_eq in e3. subst. rewrite C.cmp_opp, e2 in e1. discr. rewrite (IHx1 _ _ e1 e2) in e3. discr. Qed.
imports: Coq(Relations) CoLoR(VecUtil LogicUtil OrdUtil NatUtil)