proposition: Lemma OCPSortedTl : forall (l : list positive), StronglySorted (fun x x0 : positive => is_true (x <=? x0)%positive) l -> StronglySorted (fun x x0 : positive => is_true (x <=? x0)%positive) (tl l).
proof: Proof. intros l HSorted. induction l. simpl; apply SSorted_nil. clear IHl. simpl; apply StronglySorted_inv in HSorted; destruct HSorted as [HSorted Hhd]. assumption. Qed.
imports: MSets Arith NArith Notations Sorting Coq.Program.Equality GeoCoq.Tactics.Coinc.tactics_axioms