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