proposition: Lemma ltTrans : Transitive ltST.
proof: Proof. unfold lt. intros x y z Hxy Hyz. assert (lx : (S (S n)) = (S (S n))) by reflexivity. assert (lx' := lengthOfCPToList x). assert (lx'' := sortOK (S (S n)) (CPToList x)). rewrite <- lx' in lx''; clear lx'. apply lx'' in lx; clear lx''. assert (ly : (S (S n)) = (S (S n))) by reflexivity. assert (ly' := lengthOfCPToList y). assert (ly'' := sortOK (S (S n)) (CPToList y)). rewrite <- ly' in ly''; clear ly'. apply ly'' in ly; clear ly''. assert (lz : (S (S n)) = (S (S n))) by reflexivity. assert (lz' := lengthOfCPToList z). assert (lz'' := sortOK (S (S n)) (CPToList z)). rewrite <- lz' in lz''; clear lz'. apply lz'' in lz; clear lz''. assert (H := ltListTrans (S n) (sort (CPToList x)) (sort (CPToList y)) (sort (CPToList z))). apply H; assumption. Qed.
imports: MSets Arith NArith Notations Sorting Coq.Program.Equality GeoCoq.Tactics.Coinc.tactics_axioms