proposition: Lemma lengthAtLeastOne : forall (l : list positive) n, length l = (S n) -> exists a0 l0, l = a0 :: l0.
proof: Proof. intros l n Hl. induction l. simpl in Hl; discriminate. exists a; exists l; reflexivity. Qed.
imports: MSets Arith NArith Notations Sorting Coq.Program.Equality GeoCoq.Tactics.Coinc.tactics_axioms